Commit 2025-02-13 08:21 f2ac3318

View on Github →

feat(LocalizedModule): expand API (#20340)

Estimated changes

Modified Mathlib/Algebra/Module/LocalizedModule/IsLocalization.lean

added theorem IsLocalization.mk'_algebraMap_eq_mk'

added theorem IsLocalization.mk'_eq_mk'

modified theorem isLocalizedModule_iff_isLocalization'

modified theorem isLocalizedModule_iff_isLocalization

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

added theorem Submodule.localized'_eq_span

added theorem Submodule.localized'_smul

added def Submodule.localized'gi

added theorem Submodule.localized₀_smul

added theorem Submodule.restrictScalars_localized'_smul

Modified Mathlib/RingTheory/LocalProperties/Basic.lean

Modified scripts/nolints_prime_decls.txt