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