Commit 2023-02-08 08:06 c8a4c638

View on Github →

feat: port RingTheory.OreLocalization.Basic (#1964) The proofs in mathlib use noncomm_ring and assoc_rw.

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/OreLocalization/Basic.lean

added theorem OreLocalization.add_oreDiv

added theorem OreLocalization.div_one_mul

added def OreLocalization.liftExpand

added theorem OreLocalization.liftExpand_of

added def OreLocalization.lift₂Expand

added theorem OreLocalization.lift₂Expand_of

added theorem OreLocalization.nontrivial_of_nonZeroDivisors

added def OreLocalization.numeratorHom

added theorem OreLocalization.numeratorHom_apply

added theorem OreLocalization.numeratorHom_inj

added def OreLocalization.numeratorUnit

added theorem OreLocalization.numerator_isUnit

added def OreLocalization.oreDiv

added def OreLocalization.oreDivAddChar'

added def OreLocalization.oreDivMulChar'

added theorem OreLocalization.oreDiv_add_char

added theorem OreLocalization.oreDiv_add_oreDiv

added theorem OreLocalization.oreDiv_eq_iff

added theorem OreLocalization.oreDiv_mul_char

added theorem OreLocalization.oreDiv_mul_oreDiv

added theorem OreLocalization.oreDiv_mul_oreDiv_comm

added def OreLocalization.oreEqv

added theorem OreLocalization.right_distrib

added def OreLocalization.universalHom

added theorem OreLocalization.universalHom_apply

added theorem OreLocalization.universalHom_commutes

added theorem OreLocalization.universalHom_unique

added def OreLocalization.universalMulHom

added theorem OreLocalization.universalMulHom_apply

added theorem OreLocalization.universalMulHom_commutes

added theorem OreLocalization.universalMulHom_unique

added theorem OreLocalization.zero_div_eq_zero

added def OreLocalization