instSubsingletonOfMulArchimedean — Mathlib

English

If MulArchimedean M holds, then FiniteMulArchimedeanClass M is a subsingleton.

Русский

Если MulArchimedean M выполняется, то FiniteMulArchimedeanClass M является одиночным (субодин), то есть все элементы равны.

LaTeX

$$$\text{Subsingleton } (FiniteMulArchimedeanClass M)$$$

Lean4

@[to_additive]
instance [MulArchimedean M] : Subsingleton (FiniteMulArchimedeanClass M) where
  allEq A
    B :=
    by
    induction A using ind with
    | mk a ha
    induction B using ind with
    | mk b hb
    simpa [mk] using MulArchimedeanClass.mk_eq_mk_of_mulArchimedean ha hb

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