English
For g,g' ∈ GL(2,R) and z ∈ ℂ, the action satisfies σ(g g') z = σ(g)(σ(g') z); i.e., the action is compatible with group multiplication.
Русский
Для любых g,g' ∈ GL(2, ℝ) и z ∈ ℂ выполняется σ(g g') z = σ(g)(σ(g') z); действие совместимо с умножением по группе.
LaTeX
$$$\\\\sigma(g g')z = \\\\sigma(g)(\\\\sigma(g')z)$$$
Lean4
theorem σ_mul (g g' : GL (Fin 2) ℝ) (z : ℂ) : σ (g * g') z = σ g (σ g' z) :=
by
simp only [σ, map_mul, Units.val_mul]
rcases g.det_ne_zero.lt_or_gt with (h | h) <;> rcases g'.det_ne_zero.lt_or_gt with (h' | h')
· simp [mul_pos_of_neg_of_neg h h', h.not_gt, h'.not_gt]
· simp [(mul_neg_of_neg_of_pos h h').not_gt, h.not_gt, h']
· simp [(mul_neg_of_pos_of_neg h h').not_gt, h, h'.not_gt]
· simp [mul_pos h h', h, h']
