Commit 2025-12-19 18:36 4458a06c

View on Github →

feat(RingTheory): prerequisites for #30736 (#33095)

Estimated changes

Modified Mathlib/Algebra/Algebra/Bilinear.lean

added def LinearMap.mul''

Modified Mathlib/Algebra/Algebra/Operations.lean

added theorem Submodule.ker_unitsMap_spanSingleton

added theorem Submodule.mker_spanSingleton

added theorem Submodule.mul_top_eq_top_of_mul_eq_one

added def Submodule.span.ringHom

added def Submodule.spanSingleton

added theorem Submodule.spanSingleton_apply

added theorem Submodule.span_singleton_algebraMap_of_isUnit

added theorem Submodule.span_singleton_eq_one_iff

added theorem Submodule.top_mul_eq_top_of_mul_eq_one

Modified Mathlib/Data/Set/Semiring.lean

added def SetSemiring.singletonMonoidHom

Modified Mathlib/LinearAlgebra/Span/Defs.lean

added theorem Submodule.eq_span_singleton_of_surjective

Modified Mathlib/RingTheory/ClassGroup.lean

Modified Mathlib/RingTheory/FractionalIdeal/Basic.lean

Modified Mathlib/RingTheory/FractionalIdeal/Operations.lean

added def FractionalIdeal.unitsMulEquivSubmodule

added theorem Units.submodule_isFractional

Modified Mathlib/RingTheory/Localization/Defs.lean

added theorem IsLocalization.smul_bijective

Modified docs/references.bib