Commit 2024-08-21 14:51 93828f4c

View on Github →

chore(*): use rfl for more proofs (#16033)

Estimated changes

Modified Mathlib/Algebra/Algebra/Equiv.lean

modified theorem AlgEquiv.arrowCongr_refl

modified theorem AlgEquiv.autCongr_refl

modified theorem AlgEquiv.equivCongr_refl

modified theorem AlgEquiv.toLinearEquiv_ofLinearEquiv

Modified Mathlib/Algebra/Algebra/Hom.lean

Modified Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean

Modified Mathlib/Algebra/Algebra/Subalgebra/Basic.lean

Modified Mathlib/Algebra/Lie/Basic.lean

modified theorem LieHom.comp_id

modified theorem LieHom.id_comp

Modified Mathlib/Algebra/Module/LinearMap/Defs.lean

Modified Mathlib/LinearAlgebra/Multilinear/Basic.lean

Modified Mathlib/ModelTheory/Substructures.lean