chore(*/equiv): missing refl_symm lemmas (#13761)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
leanprover-community · Apr 28, 2022 · 1c92dfd · 1c92dfd
1 parent 0cb20fc
commit 1c92dfd
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 0 deletions.
diff --git a/src/algebra/algebra/basic.lean b/src/algebra/algebra/basic.lean
@@ -921,6 +921,9 @@ symm_bijective.injective $ ext $ λ x, rfl
   { to_fun := f', inv_fun := f,
     ..(⟨f, f', h₁, h₂, h₃, h₄, h₅⟩ : A₁ ≃ₐ[R] A₂).symm } := rfl
 
+@[simp]
+theorem refl_symm : (alg_equiv.refl : A₁ ≃ₐ[R] A₁).symm = alg_equiv.refl := rfl
+
 /-- Algebra equivalences are transitive. -/
 @[trans]
 def trans (e₁ : A₁ ≃ₐ[R] A₂) (e₂ : A₂ ≃ₐ[R] A₃) : A₁ ≃ₐ[R] A₃ :=

diff --git a/src/algebra/hom/equiv.lean b/src/algebra/hom/equiv.lean
@@ -229,6 +229,9 @@ theorem symm_mk (f : M → N) (g h₁ h₂ h₃) :
   (mul_equiv.mk f g h₁ h₂ h₃).symm =
   { to_fun := g, inv_fun := f, ..(mul_equiv.mk f g h₁ h₂ h₃).symm} := rfl
 
+@[simp, to_additive]
+theorem refl_symm : (refl M).symm = refl M := rfl
+
 /-- Transitivity of multiplication-preserving isomorphisms -/
 @[trans, to_additive "Transitivity of addition-preserving isomorphisms"]
 def trans (h1 : M ≃* N) (h2 : N ≃* P) : (M ≃* P) :=

diff --git a/src/algebra/lie/basic.lean b/src/algebra/lie/basic.lean
@@ -418,6 +418,9 @@ by { ext, refl }
 @[simp] lemma symm_apply_apply (e : L₁ ≃ₗ⁅R⁆ L₂) : ∀ x, e.symm (e x) = x :=
   e.to_linear_equiv.symm_apply_apply
 
+@[simp]
+theorem refl_symm : (refl : L₁ ≃ₗ⁅R⁆ L₁).symm = refl := rfl
+
 /-- Lie algebra equivalences are transitive. -/
 @[trans]
 def trans (e₁ : L₁ ≃ₗ⁅R⁆ L₂) (e₂ : L₂ ≃ₗ⁅R⁆ L₃) : L₁ ≃ₗ⁅R⁆ L₃ :=