out_top — Mathlib

English

The underlying value of the top element, when projected to the underlying unit, equals 1: (⊤ : MulArchimedeanClass M).out = 1.

Русский

Верхний элемент при приведении к базовой единице имеет значение 1: (⊤ : MulArchimedeanClass M).out = 1.

LaTeX

$$$(\top : MulArchimedeanClass M).out = 1$$$

Lean4

@[to_additive (attr := simp)]
theorem out_top : (⊤ : MulArchimedeanClass M).out = 1 := by rw [← mk_eq_top_iff, mk_out]

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