Commit 2026-01-03 21:36 08d60a80

View on Github →

feat(Algebra): characterise when a submodule constructor is equal to ⊥ (#32836)

Estimated changes

Modified Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean

added theorem NonUnitalAlgebra.toNonUnitalSubring_eq_top

added theorem NonUnitalAlgebra.toNonUnitalSubring_top

modified theorem NonUnitalAlgebra.toNonUnitalSubsemiring_eq_top

modified theorem NonUnitalAlgebra.toSubmodule_eq_top

deleted theorem NonUnitalAlgebra.to_subring_eq_top

deleted theorem NonUnitalAlgebra.top_toSubring

modified theorem NonUnitalSubalgebra.toNonUnitalSubsemiring_inj

modified theorem NonUnitalSubalgebra.toNonUnitalSubsemiring_injective

modified theorem NonUnitalSubalgebra.toSubmodule_inj

modified theorem NonUnitalSubalgebra.toSubmodule_injective

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

added theorem Submonoid.mk_eq_bot

added theorem Submonoid.mk_eq_top

added theorem Submonoid.toSubsemigroup_inj

added theorem Submonoid.toSubsemigroup_injective

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

added theorem Subsemigroup.mk_eq_bot

added theorem Subsemigroup.mk_eq_top

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

added theorem Submodule.mk_eq_bot

added theorem Submodule.mk_eq_top

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

added theorem Subring.toAddSubgroup_eq_top

added theorem Subring.toAddSubgroup_top

added theorem Subring.toSubsemiring_eq_top

added theorem Subring.toSubsemiring_top

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

modified theorem Subring.toAddSubgroup_injective

modified theorem Subring.toSubmonoid_injective

added theorem Subring.toSubsemiring_inj

modified theorem Subring.toSubsemiring_injective

Modified Mathlib/RingTheory/NonUnitalSubring/Basic.lean

added theorem NonUnitalSubring.toAddSubgroup_eq_top

added theorem NonUnitalSubring.toAddSubgroup_top

added theorem NonUnitalSubring.toNonUnitalSubsemiring_eq_top

added theorem NonUnitalSubring.toNonUnitalSubsemiring_top

Modified Mathlib/RingTheory/NonUnitalSubsemiring/Defs.lean

added theorem NonUnitalSubsemiring.toAddSubmonoid_eq_top

added theorem NonUnitalSubsemiring.toAddSubmonoid_inj

modified theorem NonUnitalSubsemiring.toAddSubmonoid_injective

added theorem NonUnitalSubsemiring.toAddSubmonoid_top

modified theorem NonUnitalSubsemiring.toSubsemigroup_injective