Commit 2024-10-15 06:04 74b17a17

View on Github →

chore(RingTheory/OreLocalization): split into GroupTheory.OreLocalization (#17730) The files Mathlib/GroupTheory/OreLocalization/OreSet.lean and Mathlib/GroupTheory/OreLocalization/Basic.lean contain the results of Mathlib/RingTheory/OreLocalization/OreSet.lean and Mathlib/RingTheory/OreLocalization/Basic.lean that don't involve rings or monoids with zero.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/GroupTheory/MonoidLocalization/Basic.lean

Modified Mathlib/GroupTheory/MonoidLocalization/MonoidWithZero.lean

Created Mathlib/GroupTheory/OreLocalization/Basic.lean

added def OreLocalization.liftExpand

added theorem OreLocalization.liftExpand_of

added def OreLocalization.lift₂Expand

added theorem OreLocalization.lift₂Expand_of

added theorem OreLocalization.mul_div_one

added def OreLocalization.numeratorHom

added theorem OreLocalization.numeratorHom_apply

added def OreLocalization.numeratorUnit

added theorem OreLocalization.numerator_isUnit

added def OreLocalization.oreDiv

added def OreLocalization.oreDivMulChar'

added def OreLocalization.oreDivSMulChar'

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 theorem OreLocalization.oreDiv_one_smul

added theorem OreLocalization.oreDiv_smul_char

added theorem OreLocalization.oreDiv_smul_oreDiv

added def OreLocalization.oreEqv

added theorem OreLocalization.smul_div_one

added theorem OreLocalization.smul_one_oreDiv_one_smul

added theorem OreLocalization.smul_one_smul

added theorem OreLocalization.smul_oreDiv

added theorem OreLocalization.smul_oreDiv_one

added def OreLocalization.universalMulHom

added theorem OreLocalization.universalMulHom_apply

added theorem OreLocalization.universalMulHom_commutes

added theorem OreLocalization.universalMulHom_unique

added def OreLocalization

Created Mathlib/GroupTheory/OreLocalization/OreSet.lean

added def OreLocalization.oreCondition

added def OreLocalization.oreDenom

added def OreLocalization.oreNum

added theorem OreLocalization.ore_eq

added theorem OreLocalization.ore_right_cancel

Modified Mathlib/RingTheory/OreLocalization/Basic.lean

deleted def OreLocalization.liftExpand

deleted theorem OreLocalization.liftExpand_of

deleted def OreLocalization.lift₂Expand

deleted theorem OreLocalization.lift₂Expand_of

deleted theorem OreLocalization.mul_div_one

deleted def OreLocalization.numeratorHom

deleted theorem OreLocalization.numeratorHom_apply

deleted def OreLocalization.numeratorUnit

deleted theorem OreLocalization.numerator_isUnit

deleted def OreLocalization.oreDiv

deleted def OreLocalization.oreDivMulChar'

deleted def OreLocalization.oreDivSMulChar'

deleted theorem OreLocalization.oreDiv_eq_iff

deleted theorem OreLocalization.oreDiv_mul_char

deleted theorem OreLocalization.oreDiv_mul_oreDiv

deleted theorem OreLocalization.oreDiv_mul_oreDiv_comm

deleted theorem OreLocalization.oreDiv_one_smul

deleted theorem OreLocalization.oreDiv_smul_char

deleted theorem OreLocalization.oreDiv_smul_oreDiv

deleted def OreLocalization.oreEqv

deleted theorem OreLocalization.smul_div_one

deleted theorem OreLocalization.smul_one_oreDiv_one_smul

deleted theorem OreLocalization.smul_one_smul

deleted theorem OreLocalization.smul_oreDiv

deleted theorem OreLocalization.smul_oreDiv_one

deleted def OreLocalization.universalMulHom

deleted theorem OreLocalization.universalMulHom_apply

deleted theorem OreLocalization.universalMulHom_commutes

deleted theorem OreLocalization.universalMulHom_unique

deleted def OreLocalization

Modified Mathlib/RingTheory/OreLocalization/OreSet.lean

deleted def OreLocalization.oreCondition

deleted def OreLocalization.oreDenom

deleted def OreLocalization.oreNum

deleted theorem OreLocalization.ore_eq

deleted theorem OreLocalization.ore_right_cancel