Commit 2025-02-20 15:59 0f89f3c1

View on Github →

fix: initialize_simps_projections print warning when projection data already exists (#20339)

Estimated changes

Modified Mathlib/LinearAlgebra/AffineSpace/ContinuousAffineEquiv.lean

deleted def ContinuousAffineEquiv.Simps.coe

added def ContinuousAffineEquiv.Simps.symm_apply

Modified Mathlib/Order/Category/FinPartOrd.lean

deleted def FinPartOrd.Hom.Simps.hom

Modified Mathlib/Order/Category/NonemptyFinLinOrd.lean

deleted def NonemptyFinLinOrd.Hom.Simps.hom

Modified Mathlib/RingTheory/Bialgebra/Equiv.lean

Modified Mathlib/RingTheory/Coalgebra/Equiv.lean

Modified Mathlib/Tactic/Simps/Basic.lean

Modified MathlibTest/Simps.lean