instUnique — Mathlib

English

There is a unique subalgebra of R over itself, i.e., Subalgebra R R has a single instance.

Русский

Существует единственный подалгебра над собой: Subalgebra R R имеет единственный экзепляр.

LaTeX

$$$ \\text{Subalgebra.instUnique} : \\mathrm{Unique} (\\mathrm{Subalgebra} \\ R \\ R) $$$

Lean4

instance : Unique (Subalgebra R R) :=
  { inferInstanceAs (Inhabited (Subalgebra R R)) with
    uniq := by
      intro S
      refine le_antisymm ?_ bot_le
      intro _ _
      simp only [Set.mem_range, mem_bot, algebraMap_self_apply, exists_apply_eq_apply, default] }

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