Commit 2024-07-31 09:27 012ddf4e

View on Github →

chore: improve some ext_iff lemmas (#15340) These will be auto-generated by @[ext] in lean v4.11; this prepares us for that change.

Estimated changes

deleted theorem Units.ext_iff
deleted theorem LieModule.Weight.ext_iff
deleted theorem LinearMap.ext_iff
deleted theorem MvPolynomial.ext_iff
deleted theorem NonUnitalRingHom.ext_iff
deleted theorem RingHom.ext_iff
deleted theorem NormedAddGroupHom.ext_iff
deleted theorem Complex.ext_iff
deleted theorem Finsupp.unique_ext_iff
deleted theorem AList.ext_iff
deleted theorem Prod.ext_iff
deleted theorem Set.ext_iff
deleted theorem Sigma.ext_iff
deleted theorem Subtype.ext_iff
deleted theorem CircleDeg1Lift.ext_iff
deleted theorem MulActionHom.ext_iff
deleted theorem AlternatingMap.ext_iff
deleted theorem MultilinearMap.ext_iff
deleted theorem Equiv.Perm.ext_iff