Commit 2024-06-06 10:40 a34346ed

View on Github →

refactor(RingTheory/OreLocalization): Ore localization of modules (#13151) To accommodate this change, right ore condition has been changed to left ore. This enables us to redefine Localization and LocalizedModule with OreLocalization in the future.

Estimated changes

Modified Mathlib/LinearAlgebra/Dimension/Localization.lean

Modified Mathlib/RingTheory/OreLocalization/Basic.lean

modified theorem OreLocalization.add_oreDiv

deleted theorem OreLocalization.div_one_mul

modified def OreLocalization.liftExpand

modified theorem OreLocalization.liftExpand_of

modified def OreLocalization.lift₂Expand

modified theorem OreLocalization.lift₂Expand_of

added theorem OreLocalization.mul_div_one

added theorem OreLocalization.nontrivial_iff

modified theorem OreLocalization.nontrivial_of_nonZeroDivisors

modified theorem OreLocalization.numeratorHom_inj

modified def OreLocalization.oreDiv

modified def OreLocalization.oreDivAddChar'

added def OreLocalization.oreDivSMulChar'

added theorem OreLocalization.oreDiv_add_char'

modified theorem OreLocalization.oreDiv_add_char

modified theorem OreLocalization.oreDiv_add_oreDiv

modified theorem OreLocalization.oreDiv_eq_iff

modified theorem OreLocalization.oreDiv_mul_char

modified theorem OreLocalization.oreDiv_mul_oreDiv

added theorem OreLocalization.oreDiv_one_smul

added theorem OreLocalization.oreDiv_smul_char

added theorem OreLocalization.oreDiv_smul_oreDiv

modified def OreLocalization.oreEqv

modified theorem OreLocalization.right_distrib

added theorem OreLocalization.smul_div_one

added theorem OreLocalization.smul_oreDiv

added theorem OreLocalization.subsingleton_iff

deleted theorem OreLocalization.zero_div_eq_zero

added theorem OreLocalization.zero_oreDiv

modified def OreLocalization

Modified Mathlib/RingTheory/OreLocalization/OreSet.lean

modified def OreLocalization.oreCondition

modified theorem OreLocalization.ore_eq

deleted theorem OreLocalization.ore_left_cancel

added theorem OreLocalization.ore_right_cancel