English
For nonempty intervals s and t in a commutative group α with a compatible order, the product s t equals 1 if and only if s and t are singletons and their product is 1; i.e., there exist a,b with s = pure a, t = pure b, and a b = 1.
Русский
Для непустых интервалов s и t в коммутативной группе α с совместимым порядком произведение s t равно 1 тогда и только тогда, когда оба интервала являются одноэлементными, и их элементы умножаются в единицу: ∃ a,b: s = pure a, t = pure b, a b = 1.
LaTeX
$$$ s t = 1 \iff \exists a\, b,\ s = \operatorname{pure} a \land t = \operatorname{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
refine ⟨fun h => ?_, ?_⟩
· rw [NonemptyInterval.ext_iff, Prod.ext_iff] at h
have := (mul_le_mul_iff_of_ge s.fst_le_snd t.fst_le_snd).1 (h.2.trans h.1.symm).le
refine ⟨s.fst, t.fst, ?_, ?_, h.1⟩ <;> apply NonemptyInterval.ext <;> dsimp [pure]
· nth_rw 2 [this.1]
· nth_rw 2 [this.2]
· rintro ⟨b, c, rfl, rfl, h⟩
rw [pure_mul_pure, h, pure_one]
