Theorems · Theorem · group theory

Matrix.SpecialLinearGroup.diag2_coe

∀ {F : Type u_1} [inst : Field F] (a : F) (ha : a ≠ 0),
  ↑(Matrix.SpecialLinearGroup.diag2 a ha) =
    Matrix.diagonal fun i =>
      match i with
      | 0 => a
      | 1 => a⁻¹

Defined in: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Cited by: 5 results in Mathlib
Foundations: Depth 93 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.

Cites5

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
Matrixstatement · cited by 4,303
Matrix.detstatement · cited by 665
Matrix.diagonalstatement · cited by 314
Matrix.SpecialLinearGroup.diag2statement · cited by 13

Cited by5

Results whose statement or proof uses this declaration.

Matrix.SpecialLinearGroup.diag2_mul_invproof · cited by 1
Matrix.commutator_diag2_transvectionproof · cited by 1
Matrix.transvection_mem_commutator₁proof · cited by 1
Matrix.SpecialLinearGroup.diag2_smul_single_i₁proof · cited by 0
Matrix.SpecialLinearGroup.diag2_smul_single_i₂proof · cited by 0