Mathlib Map

Theorems · Theorem · group theory

ModularGroup.coe_T_inv

↑ModularGroup.T⁻¹ = !![1, -1; 0, 1]
Defined in
Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Cited by
1 results in Mathlib
Foundations
Depth 102 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

ModularGroup.coe_T_zpow · cited by 9ModularGroup.coe_T_zpowDFunLike.coe · cited by 62936DFunLike.coeEquiv · cited by 8337EquivMatrix · cited by 4303MatrixMatrix.vecCons · cited by 852Matrix.vecConsMatrix.vecEmpty · cited by 832Matrix.vecEmptyMatrix.det · cited by 665Matrix.detneg_zero · cited by 542neg_zeroMatrix.SpecialLinearGroup · cited by 348Matrix.SpecialLinearGroupMatrix.of · cited by 336Matrix.ofMatrix.cons_val_fin_one · cited by 225Matrix.cons_val_fin_oneMatrix.cons_val' · cited by 88Matrix.cons_val'ModularGroup.T · cited by 48ModularGroup.TMatrix.adjugate_fin_two · cited by 3Matrix.adjugate_fin_twoModularGroup.coe_T_invCITED BYCITES

Cites13

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

Cited by1

Results whose statement or proof uses this declaration.