Commit 2024-08-17 20:08 220ac01a

View on Github →

chore(*): use rfl to prove symm_symm (#15923)

Estimated changes

modified theorem AlgEquiv.symm_symm
modified theorem ComplexShape.symm_symm
modified theorem LieEquiv.symm_symm
modified theorem LieModuleEquiv.symm_symm
modified theorem LinearEquiv.symm_symm
modified theorem OrderRingIso.symm_symm
modified theorem RingEquiv.symm_symm
modified theorem StarAlgEquiv.symm_symm
modified theorem StarRingEquiv.symm_symm
modified theorem PEquiv.symm_symm
modified theorem Equiv.symm_symm
modified theorem Equiv.symm_symm_apply
modified theorem PartialEquiv.symm_symm
modified theorem OrderIso.symm_symm