Theorems · Theorem · group theory

Matrix.diag2_decompose

∀ {F : Type u_1} [inst : Field F] (a : F) (ha : a ≠ 0),
  Matrix.SpecialLinearGroup.diag2 a ha =
    Matrix.SpecialLinearGroup.transvection ⋯ a * Matrix.SpecialLinearGroup.transvection ⋯ (-a⁻¹) *
            Matrix.SpecialLinearGroup.transvection ⋯ a *
          Matrix.SpecialLinearGroup.transvection ⋯ (-1) *
        Matrix.SpecialLinearGroup.transvection ⋯ 1 *
      Matrix.SpecialLinearGroup.transvection ⋯ (-1)

Defined in: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Cited by: 1 results in Mathlib
Foundations: Depth 94 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Field

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites34

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Fieldstatement and proof · cited by 7,404
mul_oneproof · cited by 3,885
one_mulproof · cited by 2,841
add_zeroproof · cited by 2,707
zero_addproof · cited by 2,366
neg_negproof · cited by 960
one_ne_zerostatement and proof · cited by 885
Matrix.vecConsproof · cited by 852
Matrix.vecEmptyproof · cited by 832
neg_mulproof · cited by 654
mul_negproof · cited by 590
mul_addproof · cited by 413

Cited by1

Results whose statement or proof uses this declaration.

Matrix.SL2.transvection_inductionproof · cited by 2