mem_unitsFstOne — Mathlib

English

An element x of Units(Unitization R A) lies in the subgroup unitsFstOne R A if and only if its first component is 1.

Русский

Элемент x из Units(Unitization R A) принадлежит подгруппе unitsFstOne R A тогда и только тогда, когда первая компонента x равна 1.

LaTeX

$$$$ x \in unitsFstOne(R,A) \iff x.val.fst = 1 $$$$

Lean4

@[simp]
theorem mem_unitsFstOne {x : (Unitization R A)ˣ} : x ∈ unitsFstOne R A ↔ x.val.fst = 1 :=
  Iff.rfl

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