Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-17 21:26 65ec5990

View on Github →

chore(linear_algebra/matrix): Use the new matrix notation in most places (#15306)

Estimated changes

Modified src/algebra/lie/cartan_matrix.lean

modified def cartan_matrix.E₆

modified def cartan_matrix.E₇

modified def cartan_matrix.E₈

modified def cartan_matrix.F₄

modified def cartan_matrix.G₂

Modified src/analysis/complex/isometry.lean

Modified src/analysis/special_functions/polar_coord.lean

Modified src/data/complex/determinant.lean

Modified src/data/complex/module.lean

Modified src/data/fin/vec_notation.lean

Modified src/data/matrix/notation.lean

added theorem matrix.cons_vec_mul_cons

added theorem matrix.eta_fin_three

added theorem matrix.eta_fin_two

Modified src/linear_algebra/general_linear_group.lean

Modified src/linear_algebra/matrix/adjugate.lean

deleted theorem matrix.adjugate_fin_two'

added theorem matrix.adjugate_fin_two_of

Modified src/linear_algebra/matrix/determinant.lean

deleted theorem matrix.det_fin_one_mk

added theorem matrix.det_fin_one_of

Modified src/linear_algebra/matrix/to_lin.lean

Modified src/number_theory/modular.lean

modified def modular_group.S

modified def modular_group.T

modified theorem modular_group.coe_S

modified theorem modular_group.coe_T

modified theorem modular_group.coe_T_inv

modified theorem modular_group.coe_T_zpow

Modified src/topology/algebra/module/finite_dimension.lean