Commit 2024-11-28 19:53 f60ba8f8

View on Github →

chore: tag all closure_mono lemmas gcongr (#19561) From GrowthInGroups (LeanCamCombi)

Estimated changes

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

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

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

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

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

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

Modified Mathlib/Data/Matroid/Closure.lean

Modified Mathlib/Deprecated/Subfield.lean

Modified Mathlib/Deprecated/Subgroup.lean

Modified Mathlib/Deprecated/Submonoid.lean

Modified Mathlib/Deprecated/Subring.lean

Modified Mathlib/ModelTheory/Substructures.lean

Modified Mathlib/RingTheory/NonUnitalSubring/Basic.lean

Modified Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean