Commit 2025-07-19 04:00 261ed06a

View on Github →

feat: add new simp lemmas (#26175) Split from #25961 so that performance issues can be investigated.

Estimated changes

Modified Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean

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

Modified Mathlib/Algebra/Field/Subfield/Defs.lean

Modified Mathlib/Algebra/Group/Subgroup/Basic.lean

Modified Mathlib/Algebra/Group/Subgroup/Lattice.lean

Modified Mathlib/Algebra/Group/Submonoid/Defs.lean

Modified Mathlib/Algebra/Group/Submonoid/Pointwise.lean

Modified Mathlib/Algebra/Lie/Subalgebra.lean

Modified Mathlib/Algebra/Lie/Submodule.lean

Modified Mathlib/Algebra/Module/Bimodule.lean

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

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

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

Modified Mathlib/Algebra/Ring/Subring/Basic.lean

Modified Mathlib/Algebra/Ring/Subring/Defs.lean

Modified Mathlib/Algebra/Ring/Subsemiring/Defs.lean

Modified Mathlib/Algebra/Star/NonUnitalSubalgebra.lean

Modified Mathlib/Algebra/Star/Subalgebra.lean

Modified Mathlib/Analysis/Normed/Group/Quotient.lean

Modified Mathlib/FieldTheory/IntermediateField/Basic.lean

modified theorem IntermediateField.natCast_mem

Modified Mathlib/GroupTheory/Nilpotent.lean

Modified Mathlib/LinearAlgebra/RootSystem/WeylGroup.lean

Modified Mathlib/LinearAlgebra/Span/Defs.lean

Modified Mathlib/NumberTheory/KummerDedekind.lean

Modified Mathlib/RingTheory/DedekindDomain/AdicValuation.lean

Modified Mathlib/RingTheory/DedekindDomain/Different.lean

Modified Mathlib/RingTheory/EssentialFiniteness.lean

Modified Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean

Modified Mathlib/RingTheory/NonUnitalSubring/Basic.lean

Modified Mathlib/RingTheory/TwoSidedIdeal/Basic.lean

Modified Mathlib/Topology/Algebra/Algebra.lean

Modified Mathlib/Topology/Algebra/InfiniteSum/Nonarchimedean.lean

Modified Mathlib/Topology/Algebra/NonUnitalAlgebra.lean

Modified Mathlib/Topology/Algebra/NonUnitalStarAlgebra.lean

Modified Mathlib/Topology/Algebra/StarSubalgebra.lean

Modified Mathlib/Topology/Category/Profinite/Nobeling/Basic.lean