oreSetComm — Mathlib

English

Every submonoid of a commutative monoid is an Ore set.

Русский

Любое подмономиод в коммутативном моноиде является множеством Оре.

LaTeX

$$OreSet Comm : If R is commutative, then for any S ⊆ R, S is an OreSet$$

Lean4

/-- Every submonoid of a commutative monoid is an Ore set. -/
@[to_additive AddOreLocalization.addOreSetComm]
instance (priority := 100) oreSetComm {R} [CommMonoid R] (S : Submonoid R) : OreSet S
    where
  ore_right_cancel m n s h := ⟨s, by rw [mul_comm (s : R) n, mul_comm (s : R) m, h]⟩
  oreNum r _ := r
  oreDenom _ s := s
  ore_eq r s := by rw [mul_comm]

Похожие утверждения