isUnit_iff — Mathlib

English

For any pair (a,b) in M × N, IsUnit(a,b) holds if and only if IsUnit(a) and IsUnit(b).

Русский

Для пары (a,b) ∈ M × N выполняется IsUnit(a,b) тогда и только тогда, когда IsUnit(a) и IsUnit(b).

LaTeX

$$$\\IsUnit((a,b)) \\iff \\IsUnit(a) \\wedge \\IsUnit(b)$$$

Lean4

@[to_additive]
theorem _root_.Prod.isUnit_iff {x : M × N} : IsUnit x ↔ IsUnit x.1 ∧ IsUnit x.2
    where
  mp h := ⟨(prodUnits h.unit).1.isUnit, (prodUnits h.unit).2.isUnit⟩
  mpr h := (prodUnits.symm (h.1.unit, h.2.unit)).isUnit

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