Mathlib Map

Theorems · Theorem · group theory

Matrix.SpecialLinearGroup.coe_int_neg

∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R]
  [inst_3 : Fact (Even (Fintype.card n))] (g : Matrix.SpecialLinearGroup n ℤ),
  (Matrix.SpecialLinearGroup.map (Int.castRingHom R)) (-g) = -(Matrix.SpecialLinearGroup.map (Int.castRingHom R)) g
Defined in
Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Cited by
2 results in Mathlib
Foundations
Depth 100 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
DecidableEqFintypeCommRingFact
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

ModularGroup.SL_neg_smul · cited by 5ModularGroup.SL_neg_smulModularForm.levelOne_odd_weight_eq_zero · cited by 1ModularForm.levelOne_odd_…DFunLike.coe · cited by 62936DFunLike.coeCommRing · cited by 17173CommRingFintype · cited by 7736FintypeMonoidHom · cited by 3629MonoidHomFact · cited by 2726FactFintype.card · cited by 1386Fintype.cardEven · cited by 444EvenMatrix.SpecialLinearGroup · cited by 348Matrix.SpecialLinearGroupInt.castRingHom · cited by 254Int.castRingHomMatrix.SpecialLinearGroup.map · cited by 77SpecialLinearGroup.mapRingHom.mapMatrix · cited by 55RingHom.mapMatrixRingHom.map_neg · cited by 10RingHom.map_negSpecialLinearGroup.coe_int_negCITED BYCITES

Cites12

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

Cited by2

Results whose statement or proof uses this declaration.