Commit 2023-05-23 07:30 a4dbf4c4

View on Github →

feat: port LinearAlgebra.Matrix.SpecialLinearGroup (#3710)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean

added theorem Matrix.SpecialLinearGroup.SL2_inv_expl

added theorem Matrix.SpecialLinearGroup.SL2_inv_expl_det

added theorem Matrix.SpecialLinearGroup.coe_int_neg

added theorem Matrix.SpecialLinearGroup.coe_inv

added theorem Matrix.SpecialLinearGroup.coe_matrix_coe

added theorem Matrix.SpecialLinearGroup.coe_mk

added theorem Matrix.SpecialLinearGroup.coe_mul

added theorem Matrix.SpecialLinearGroup.coe_neg

added theorem Matrix.SpecialLinearGroup.coe_one

added theorem Matrix.SpecialLinearGroup.coe_pow

added theorem Matrix.SpecialLinearGroup.coe_toGL

added theorem Matrix.SpecialLinearGroup.det_coe

added theorem Matrix.SpecialLinearGroup.det_ne_zero

added theorem Matrix.SpecialLinearGroup.ext

added theorem Matrix.SpecialLinearGroup.ext_iff

added theorem Matrix.SpecialLinearGroup.fin_two_exists_eq_mk_of_apply_zero_one_eq_zero

added theorem Matrix.SpecialLinearGroup.fin_two_induction

added def Matrix.SpecialLinearGroup.map

added theorem Matrix.SpecialLinearGroup.row_ne_zero

added def Matrix.SpecialLinearGroup.toGL

added def Matrix.SpecialLinearGroup.toLin'

added theorem Matrix.SpecialLinearGroup.toLin'_apply

added theorem Matrix.SpecialLinearGroup.toLin'_injective

added theorem Matrix.SpecialLinearGroup.toLin'_symm_apply

added theorem Matrix.SpecialLinearGroup.toLin'_symm_to_linearMap

added theorem Matrix.SpecialLinearGroup.toLin'_to_linearMap

added def Matrix.SpecialLinearGroup

added def ModularGroup.S

added def ModularGroup.T

added theorem ModularGroup.T_inv_mul_apply_one

added theorem ModularGroup.T_mul_apply_one

added theorem ModularGroup.T_pow_mul_apply_one

added theorem ModularGroup.coe_S

added theorem ModularGroup.coe_T

added theorem ModularGroup.coe_T_inv

added theorem ModularGroup.coe_T_zpow