instNontrivialUnitsOfDenselyOrdered

English

If α is densely ordered, then αˣ is nontrivial.

Русский

Если α densely ordered, то αˣ ненулевой (нетривиальная).

LaTeX

$$$DenselyOrdered \\\\alpha \\\\Rightarrow Nontrivial (\\\\alpha^{\\\\times})$$$

Lean4

instance [DenselyOrdered α] : Nontrivial αˣ :=
  have := denselyOrdered_iff_denselyOrdered_units_and_nontrivial_units (α := α)
  by
  tauto
    -- Counterexample with monoid:
    -- `{ x : ℝ | x = 0 ∨ ∃ (a : ℤ) (b c : ℕ), x = Real.exp (a + b * √2 - c * √3) }`

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