Commit 2024-09-24 11:40 70a55654

View on Github →

refactor: Make mem_ker be simp (#17021) Do this for MonoidHom.mem_ker, MonoidHom.mem_mker, RingHom.mem_ker. This matches LinearMap.mem_ker. From LeanAPAP

Estimated changes

Modified Mathlib/Algebra/Category/Grp/Kernels.lean

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

modified theorem MonoidHom.mem_ker

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

modified theorem MonoidHom.mem_mker

Modified Mathlib/Algebra/Lie/Submodule.lean

modified theorem LieModuleHom.comp_ker_incl

modified theorem LieModuleHom.mem_ker

Modified Mathlib/GroupTheory/Abelianization.lean

Modified Mathlib/GroupTheory/PresentedGroup.lean

Modified Mathlib/GroupTheory/QuotientGroup/Basic.lean

Modified Mathlib/GroupTheory/Torsion.lean

Modified Mathlib/RingTheory/Henselian.lean

Modified Mathlib/RingTheory/Ideal/Maps.lean

modified theorem Ideal.RingHom.mem_ker

Modified Mathlib/RingTheory/Ideal/QuotientOperations.lean

Modified Mathlib/RingTheory/IsAdjoinRoot.lean

Modified Mathlib/RingTheory/Kaehler/Basic.lean

Modified Mathlib/RingTheory/Localization/Algebra.lean

Modified Mathlib/RingTheory/Polynomial/Basic.lean

Modified Mathlib/RingTheory/Smooth/Kaehler.lean