English
For A with suitable properties, we have a commutation relation: a •> (A⁻¹ A) = (A⁻¹ A) <• a.
Русский
Для A с подходящими свойствами верно отношение коммутатии: a •> (A⁻¹ A) = (A⁻¹ A) <• a.
LaTeX
$$$a \!\bullet\! (A^{-1}A) = (A^{-1}A) \!\bullet\! a$$$
Lean4
theorem smul_inv_mul_eq_inv_mul_opSMul (h : #(A * A) < (3 / 2 : ℚ) * #A) (ha : a ∈ A) :
a •> (A⁻¹ * A) = (A⁻¹ * A) <• a := by
refine subset_antisymm ?_ ?_
· rw [subset_smul_finset_iff, ← op_inv]
calc
a •> (A⁻¹ * A) <• a⁻¹ ⊆ a •> (A⁻¹ * A) * A⁻¹ := op_smul_finset_subset_mul (by simpa)
_ ⊆ A * (A⁻¹ * A) * A⁻¹ := by gcongr; exact smul_finset_subset_mul (by simpa)
_ = A⁻¹ * A := by
simp_rw [← coe_inj, coe_mul]
rw [← mul_assoc, ← invMulSubgroup_eq_mul_inv _ h, mul_assoc, ← invMulSubgroup_eq_mul_inv _ h, coe_mul_coe,
invMulSubgroup_eq_inv_mul]
· rw [subset_smul_finset_iff]
calc
a⁻¹ •> ((A⁻¹ * A) <• a) ⊆ A⁻¹ * (A⁻¹ * A) <• a := smul_finset_subset_mul (by simpa)
_ ⊆ A⁻¹ * ((A⁻¹ * A) * A) := by gcongr; exact op_smul_finset_subset_mul (by simpa)
_ = A⁻¹ * A := by
rw [← mul_inv_eq_inv_mul_of_doubling_lt_two <| weaken_doubling h]
simp_rw [← coe_inj, coe_mul]
rw [mul_assoc, ← invMulSubgroup_eq_inv_mul _ h, ← mul_assoc, ← invMulSubgroup_eq_inv_mul _ h, ←
invMulSubgroup_eq_mul_inv _ h, coe_mul_coe]
