instGroup — Mathlib

English

The set of linear changes of variables forms a group under composition.

Русский

Множество линейных преобразований переменных образует группу относительно композиции.

LaTeX

$$$\\text{The set of } \\mathrm{VariableChange}(R) \\text{ forms a group under composition.}$$$

Lean4

instance : Group (VariableChange R)
    where
  one_mul C := by simp only [mul_def, one_def, zero_add, zero_mul, mul_zero, one_mul]
  mul_one C := by simp only [mul_def, one_def, add_zero, mul_zero, one_mul, mul_one, one_pow, Units.val_one]
  inv_mul_cancel
    C := by
    rw [mul_def, one_def, inv_def]
    ext <;> dsimp only
    · exact C.u.inv_mul
    · linear_combination -C.r * pow_mul_pow_eq_one 2 C.u.inv_mul
    · linear_combination -C.s * C.u.inv_mul
    ·
      linear_combination
        (C.r * C.s - C.t) * pow_mul_pow_eq_one 3 C.u.inv_mul + -C.r * C.s * pow_mul_pow_eq_one 2 C.u.inv_mul
  mul_assoc _ _ _ := by ext <;> simp only [mul_def, Units.val_mul] <;> ring1

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