Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-09 09:20 11ced180

View on Github →

feat(algebra/lie/classical): Use computable matrix inverses where possible (#10218)

Estimated changes

Modified src/algebra/lie/classical.lean

modified theorem lie_algebra.orthogonal.PB_inv

added def lie_algebra.orthogonal.invertible_Pso

deleted theorem lie_algebra.orthogonal.is_unit_PB

deleted theorem lie_algebra.orthogonal.is_unit_PD

deleted theorem lie_algebra.orthogonal.is_unit_Pso

added def lie_algebra.orthogonal.so_indefinite_equiv

added def lie_algebra.orthogonal.type_B_equiv_so'

added def lie_algebra.orthogonal.type_D_equiv_so'

Modified src/algebra/lie/matrix.lean

added def matrix.lie_conj

modified theorem matrix.lie_conj_apply

modified theorem matrix.lie_conj_symm_apply

Modified src/algebra/lie/skew_adjoint.lean

added def skew_adjoint_matrices_lie_subalgebra_equiv

Modified src/linear_algebra/matrix/to_linear_equiv.lean

added def matrix.to_linear_equiv'

modified theorem matrix.to_linear_equiv'_apply

modified theorem matrix.to_linear_equiv'_symm_apply