mul_eq_one_iff — Mathlib

English

In a division monoid, s × t = 1 if and only if s and t are singletons {a} and {b} with a b = 1.

Русский

В дивизионном моноиде: s × t = 1 эквивалентно тому, что s = {a}, t = {b} и a b = 1.

LaTeX

$$s × t = 1 ↔ ∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1$$

Lean4

@[to_additive]
protected theorem mul_eq_one_iff : s * t = 1 ↔ ∃ a b, s = { a } ∧ t = { b } ∧ a * b = 1 := by
  simp_rw [← coe_inj, coe_mul, coe_one, Set.mul_eq_one_iff, coe_singleton]

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