oreSetBot — Mathlib

English

The trivial submonoid is an Ore set.

Русский

Пустое(минимальное) подмономиод — множество Оре.

LaTeX

$$OreSet Bot is an OreSet$$

Lean4

/-- The trivial submonoid is an Ore set. -/
@[to_additive AddOreLocalization.addOreSetBot]
instance oreSetBot : OreSet (⊥ : Submonoid R)
    where
  ore_right_cancel _ _ s
    h :=
    ⟨s, by
      rcases s with ⟨s, hs⟩
      rw [Submonoid.mem_bot] at hs
      subst hs
      rw [mul_one, mul_one] at h
      subst h
      rfl⟩
  oreNum r _ := r
  oreDenom _ s := s
  ore_eq _
    s := by
    rcases s with ⟨s, hs⟩
    rw [Submonoid.mem_bot] at hs
    simp [hs]

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