English
The congruence r on M × S is equivalent to the explicit form that uses an existential condition on a single element of S.
Русский
Связь r на M × S эквивалентна явной форме, которая использует существующее условие на элемент S.
LaTeX
$$$ r S x y \iff \exists c \in S, \; c\cdot (y_2\,x_1) = c\cdot (x_2\,y_1) $$$
Lean4
@[to_additive]
theorem r_iff_oreEqv_r {x y : M × S} : r S x y ↔ (OreLocalization.oreEqv S M).r x y :=
by
simp only [r_iff_exists, Subtype.exists, exists_prop, OreLocalization.oreEqv, smul_eq_mul, Submonoid.mk_smul]
constructor
· rintro ⟨u, hu, e⟩
exact ⟨_, mul_mem hu x.2.2, u * y.2, by rw [mul_assoc, mul_assoc, ← e], mul_right_comm _ _ _⟩
· rintro ⟨u, hu, v, e₁, e₂⟩
exact ⟨u, hu, by rw [← mul_assoc, e₂, mul_right_comm, ← e₁, mul_assoc, mul_comm y.1]⟩
