Commit 2023-03-01 18:09 9aade17b

View on Github →

fix: replace symmApply by symm_apply (#2560)

Estimated changes

Modified Mathlib/Algebra/Algebra/Equiv.lean

deleted def AlgEquiv.Simps.symmApply

added def AlgEquiv.Simps.symm_apply

Modified Mathlib/Algebra/GCDMonoid/Basic.lean

Modified Mathlib/Algebra/Group/Opposite.lean

Modified Mathlib/Algebra/GroupRingAction/Basic.lean

Modified Mathlib/Algebra/Hom/Equiv/Basic.lean

deleted def MulEquiv.Simps.symmApply

added def MulEquiv.Simps.symm_apply

deleted theorem MulHom.toMulEquiv_symmApply

added theorem MulHom.toMulEquiv_symm_apply

Modified Mathlib/Algebra/Module/Equiv.lean

deleted def LinearEquiv.Simps.symmApply

added def LinearEquiv.Simps.symm_apply

Modified Mathlib/Algebra/Module/LinearMap.lean

Modified Mathlib/Algebra/Module/Submodule/Basic.lean

Modified Mathlib/Algebra/Module/ULift.lean

Modified Mathlib/Algebra/Order/Field/Basic.lean

Modified Mathlib/Algebra/Order/Group/OrderIso.lean

Modified Mathlib/Algebra/Order/Hom/Ring.lean

deleted def OrderRingIso.Simps.symmApply

added def OrderRingIso.Simps.symm_apply

Modified Mathlib/Algebra/Order/SMul.lean

Modified Mathlib/Algebra/Ring/AddAut.lean

Modified Mathlib/Algebra/Ring/Equiv.lean

deleted def RingEquiv.Simps.symmApply

added def RingEquiv.Simps.symm_apply

Modified Mathlib/Algebra/Ring/Fin.lean

Modified Mathlib/Algebra/Ring/Prod.lean

Modified Mathlib/Data/Dfinsupp/Basic.lean

Modified Mathlib/Data/Dfinsupp/Multiset.lean

Modified Mathlib/Data/Fin/Basic.lean

Modified Mathlib/Data/Finsupp/Basic.lean

Modified Mathlib/Data/Finsupp/ToDfinsupp.lean

deleted theorem finsuppLequivDfinsupp_symmApply

added theorem finsuppLequivDfinsupp_symm_apply

Modified Mathlib/Data/Real/Basic.lean

Modified Mathlib/GroupTheory/Congruence.lean

Modified Mathlib/GroupTheory/GroupAction/Group.lean

Modified Mathlib/GroupTheory/IsFreeGroup.lean

Modified Mathlib/GroupTheory/Perm/Basic.lean

Modified Mathlib/GroupTheory/Subgroup/Basic.lean

Modified Mathlib/GroupTheory/Submonoid/Membership.lean

Modified Mathlib/GroupTheory/Submonoid/Operations.lean

Modified Mathlib/GroupTheory/Subsemigroup/Operations.lean

Modified Mathlib/LinearAlgebra/Basic.lean

Modified Mathlib/LinearAlgebra/Finsupp.lean

Modified Mathlib/LinearAlgebra/LinearIndependent.lean

Modified Mathlib/LinearAlgebra/Pi.lean

deleted theorem LinearEquiv.piRing_symmApply

added theorem LinearEquiv.piRing_symm_apply

Modified Mathlib/Logic/Equiv/Fin.lean

Modified Mathlib/Logic/Equiv/LocalEquiv.lean

deleted def LocalEquiv.Simps.symmApply

added def LocalEquiv.Simps.symm_apply

Modified Mathlib/Logic/Equiv/Set.lean

Modified Mathlib/Order/Concept.lean

Modified Mathlib/Order/Hom/Basic.lean

Modified Mathlib/Order/Hom/Set.lean

Modified Mathlib/Order/ModularLattice.lean

Modified Mathlib/Order/RelIso/Basic.lean

deleted def RelIso.Simps.symmApply

added def RelIso.Simps.symm_apply