Commit 2022-12-30 14:14 c14f67f6

View on Github →

feat: port RingTheory.OreLocalization.OreSet (#1266)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/OreLocalization/OreSet.lean

added def OreLocalization.oreCondition

added def OreLocalization.oreDenom

added def OreLocalization.oreNum

added def OreLocalization.oreSetOfCancelMonoidWithZero

added def OreLocalization.oreSetOfNoZeroDivisors

added theorem OreLocalization.ore_eq

added theorem OreLocalization.ore_left_cancel