English
For intervals s,t in Interval(α) with a commutative group structure, s t = 1 if and only if there exist a,b with s = pure a and t = pure b and a b = 1.
Русский
Для интервалов s,t в Interval(α) с коммутативной группой существует равносильность: s t = 1 тогда и только тогда, когда существуют a,b такие, что s = pure a, t = pure b и a b = 1.
LaTeX
$$$ s t = 1 \iff \exists a,b,\ s = pure a \land t = pure b \land a b = 1 $$$
Lean4
@[to_additive]
protected theorem mul_eq_one_iff : s * t = 1 ↔ ∃ a b, s = pure a ∧ t = pure b ∧ a * b = 1 :=
by
cases s
· simp
cases t
· simp
· simp_rw [← NonemptyInterval.coe_mul_interval, ← NonemptyInterval.coe_one_interval, WithBot.coe_inj,
NonemptyInterval.coe_eq_pure]
exact NonemptyInterval.mul_eq_one_iff
