isUnit_iff_isUnit_fst — Mathlib

English

An element x ∈ tsze_R M is a unit if and only if its fst-component is a unit in R.

Русский

Элемент x∈tsze_R M является единицей тогда и только тогда, когда первая координата fst(x) является единицей в R.

LaTeX

$$$ IsUnit(x) \\iff IsUnit(fst(x)) $$$

Lean4

/-- When lowered to a prop, `Matrix.invertibleEquivInvertibleFst` forms an `iff`. -/
theorem isUnit_iff_isUnit_fst {x : tsze R M} : IsUnit x ↔ IsUnit x.fst := by
  simp only [← nonempty_invertible_iff_isUnit, (invertibleEquivInvertibleFst x).nonempty_congr]

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