mul_inv_eq_inv_mul_of_doubling_lt_two

English

For any A and h, the underlying set of invMulSubgroup A h equals A⁻¹ · A.

Русский

Для любого A и h множество, задаваемое invMulSubgroup A h, равно A⁻¹ · A.

LaTeX

$$$(A\text{.invMulSubgroup} \; h) = A^{-1} A$$$

Lean4

/-- If `A` has doubling strictly less than `2`, then `A * A⁻¹ = A⁻¹ * A`. -/
theorem mul_inv_eq_inv_mul_of_doubling_lt_two (h : #(A * A) < 2 * #A) : A * A⁻¹ = A⁻¹ * A :=
  by
  refine Subset.antisymm ?_ (mul_inv_eq_inv_mul_of_doubling_lt_two_aux h)
  simpa using mul_inv_eq_inv_mul_of_doubling_lt_two_aux (A := A⁻¹) (by simpa [← mul_inv_rev] using h)

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