Commit 2025-02-13 14:10 8c0a6d45

View on Github →

chore(RingTheory/IsLocalizedModule): extend API (#21483) In particular remove @[simps] from IsLocalizedModule.iso: The definition should not be unfolded by simp. Instead one should use the ext lemmas and the two newly provided simp lemmas.

Estimated changes

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

added theorem IsLocalizedModule.iso_mk_one

added theorem IsLocalizedModule.iso_symm_apply

added theorem IsLocalizedModule.lift_comp_iso

added theorem IsLocalizedModule.lift_iso

added theorem IsLocalizedModule.linearEquiv_apply

added theorem IsLocalizedModule.linearEquiv_symm_apply

added theorem IsLocalizedModule.mem_ker_iff

added theorem IsLocalizedModule.subsingleton_iff

added theorem IsLocalizedModule.subsingleton_iff_ker_eq_top

added theorem LocalizedModule.lift_mk_one

modified theorem LocalizedModule.mem_ker_mkLinearMap_iff

modified theorem LocalizedModule.subsingleton_iff

modified theorem LocalizedModule.subsingleton_iff_ker_eq_top