Documentation Verification Report

FixedDetMatrices

📁 Source: Mathlib/LinearAlgebra/Matrix/FixedDetMatrices.lean

Statistics

Metric	Count
Definitions `instMulActionSpecialLinearGroupFixedDetMatrix`, `instSMulSpecialLinearGroupFixedDetMatrix`, `reduce`, `reduceStep`, `reduce_rec`, `reps`, `repsFintype`, `FixedDetMatrix`	8
Theorems `S_smul_four`, `T_S_rel_smul`, `ext`, `ext'`, `ext_iff`, `induction_on`, `reduce_mem_reps`, `reduce_of_not_pos`, `reduce_of_pos`, `reduce_reduceStep`, `reps_entries_le_m'`, `reps_one_id`, `reps_zero_empty`, `smul_coe`, `smul_def`, `SL2Z_generators`	16
Total	24

FixedDetMatrices

Definitions

Name	Category	Theorems
`instMulActionSpecialLinearGroupFixedDetMatrix` 📖	CompOp	—
`instSMulSpecialLinearGroupFixedDetMatrix` 📖	CompOp	6 math math: `reduce_of_pos`, `T_S_rel_smul`, `smul_def`, `reduce_of_not_pos`, `smul_coe`, `S_smul_four`
`reduce` 📖	CompOp	4 math math: `reduce_reduceStep`, `reduce_of_pos`, `reduce_mem_reps`, `reduce_of_not_pos`
`reduceStep` 📖	CompOp	1 math math: `reduce_reduceStep`
`reduce_rec` 📖	CompOp	—
`reps` 📖	CompOp	2 math math: `reps_zero_empty`, `reduce_mem_reps`
`repsFintype` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`S_smul_four` 📖	mathematical	—	`Matrix.SpecialLinearGroup` `Fin.fintype` `Int.instCommRing` `FixedDetMatrix` `instSMulSpecialLinearGroupFixedDetMatrix` `ModularGroup.S`	—	`ModularGroup.S_mul_S_eq` `neg_mul` `one_mul` `mul_neg` `neg_neg` `Subtype.coe_eta`
`T_S_rel_smul` 📖	mathematical	—	`Matrix.SpecialLinearGroup` `Fin.fintype` `Int.instCommRing` `FixedDetMatrix` `instSMulSpecialLinearGroupFixedDetMatrix` `ModularGroup.S` `ModularGroup.T` `Matrix.SpecialLinearGroup.hasInv`	—	`IsScalarTower.left`
`ext` 📖	—	`Matrix` `Matrix.det`	—	—	`ext'` `Matrix.ext`
`ext'` 📖	—	`Matrix` `Matrix.det`	—	—	—
`ext_iff` 📖	mathematical	—	`Matrix` `Matrix.det`	—	`ext`
`induction_on` 📖	—	`Matrix.SpecialLinearGroup` `Fin.fintype` `Int.instCommRing` `FixedDetMatrix` `instSMulSpecialLinearGroupFixedDetMatrix` `ModularGroup.S` `ModularGroup.T`	—	—	`reduce_mem_reps` `reduce_of_pos` `reduce_of_not_pos` `reduce_reduceStep`
`reduce_mem_reps` 📖	mathematical	—	`FixedDetMatrix` `Fin.fintype` `Int.instCommRing` `Set` `Set.instMembership` `reps` `reduce`	—	`reduce_of_pos` `Int.emod_lt_abs` `ModularGroup.coe_T_zpow` `mul_comm` `MulZeroClass.zero_mul` `abs_eq_self` `Int.instIsOrderedAddMonoid` `Matrix.cons_mul` `Matrix.empty_mul` `Equiv.symm_apply_apply` `Matrix.cons_val'` `Matrix.cons_dotProduct` `one_mul` `neg_mul` `Matrix.dotProduct_of_isEmpty` `Fin.isEmpty'` `add_zero` `zero_add` `Matrix.empty_val'` `Matrix.cons_val_fin_one` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `Int.instAddLeftMono` `ModularGroup.S_mul_S_eq` `mul_neg` `Matrix.neg_cons` `Matrix.neg_empty` `reduce_of_not_pos` `neg_neg` `MulZeroClass.mul_zero` `neg_zero` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `neg_add_rev` `abs_neg` `not_lt` `add_comm` `reduce_reduceStep`
`reduce_of_not_pos` 📖	mathematical	`Matrix` `Matrix.det` `Fin.fintype` `Int.instCommRing`	`reduce` `Matrix.SpecialLinearGroup` `FixedDetMatrix` `instSMulSpecialLinearGroupFixedDetMatrix` `DivInvMonoid.toZPow` `Group.toDivInvMonoid` `Matrix.SpecialLinearGroup.instGroup` `ModularGroup.T` `ModularGroup.S`	—	`reduce.eq_1` `zpow_neg` `neg_neg`
`reduce_of_pos` 📖	mathematical	`Matrix` `Matrix.det` `Fin.fintype` `Int.instCommRing`	`reduce` `Matrix.SpecialLinearGroup` `FixedDetMatrix` `instSMulSpecialLinearGroupFixedDetMatrix` `DivInvMonoid.toZPow` `Group.toDivInvMonoid` `Matrix.SpecialLinearGroup.instGroup` `ModularGroup.T`	—	`reduce.eq_1` `zpow_neg` `neg_neg`
`reduce_reduceStep` 📖	mathematical	—	`reduce` `reduceStep`	—	`reduce.eq_1`
`reps_entries_le_m'` 📖	mathematical	`FixedDetMatrix` `Fin.fintype` `Int.instCommRing` `Set` `Set.instMembership` `reps`	`Finset` `Finset.instMembership` `Finset.Icc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `Int.instLocallyFiniteOrder` `abs` `Int.instAddGroup` `Matrix` `Matrix.det`	—	`LE.le.trans_lt` `abs_nonneg` `Int.instAddLeftMono` `covariant_swap_add_of_covariant_add` `abs_pos` `LT.lt.ne'` `Fintype.complete` `IsStrictOrderedRing.toIsOrderedRing` `Int.instIsStrictOrderedRing` `le_mul_iff_one_le_right` `IsOrderedRing.toPosMulMono` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `LE.le.trans` `LT.lt.le` `le_mul_of_one_le_left` `IsOrderedRing.toMulPosMono` `abs_zero` `le_mul_iff_one_le_left` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Finset.mem_Icc` `abs_le` `Int.instIsOrderedAddMonoid`
`reps_one_id` 📖	mathematical	`Matrix` `Matrix.det` `Fin.fintype` `Int.instCommRing` `abs` `instLatticeInt` `Int.instAddGroup`	`Matrix.SpecialLinearGroup` `Matrix.SpecialLinearGroup.hasOne`	—	`Int.mul_eq_one_iff_eq_one_or_neg_one` `ext` `Fintype.complete` `Matrix.one_apply_eq` `Matrix.one_apply_ne` `Fin.instNeZeroHAddNatOfNat_mathlib_1` `abs_one` `IsStrictOrderedRing.toIsOrderedRing` `Int.instIsStrictOrderedRing`
`reps_zero_empty` 📖	mathematical	—	`reps` `Set` `FixedDetMatrix` `Fin.fintype` `Int.instCommRing` `Set.instEmptyCollection`	—	`reps.eq_1` `Set.eq_empty_iff_forall_notMem` `IsStrictOrderedRing.noZeroDivisors` `Int.instIsStrictOrderedRing` `AddGroup.existsAddOfLE` `LT.lt.ne'` `abs_zero` `Int.instAddLeftMono` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `neg_neg_of_pos` `Int.instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `IsStrictOrderedRing.toIsOrderedRing` `abs_nonneg` `covariant_swap_add_of_covariant_add`
`smul_coe` 📖	mathematical	—	`Matrix` `Matrix.det` `Matrix.SpecialLinearGroup` `FixedDetMatrix` `instSMulSpecialLinearGroupFixedDetMatrix` `Matrix.instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`smul_def`
`smul_def` 📖	mathematical	—	`Matrix.SpecialLinearGroup` `FixedDetMatrix` `instSMulSpecialLinearGroupFixedDetMatrix` `Matrix` `Matrix.det` `Matrix.instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	—

SpecialLinearGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`SL2Z_generators` 📖	mathematical	—	`Subgroup.closure` `Matrix.SpecialLinearGroup` `Fin.fintype` `Int.instCommRing` `Matrix.SpecialLinearGroup.instGroup` `Set` `Set.instInsert` `ModularGroup.S` `Set.instSingletonSet` `ModularGroup.T` `Top.top` `Subgroup` `Subgroup.instTop`	—	`Subgroup.eq_top_iff'` `FixedDetMatrices.induction_on` `one_ne_zero` `FixedDetMatrices.reps_one_id` `OneMemClass.one_mem` `SubmonoidClass.toOneMemClass` `SubgroupClass.toSubmonoidClass` `Subgroup.instSubgroupClass` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `Subgroup.subset_closure` `Set.mem_insert` `Set.mem_insert_of_mem`

(root)

Definitions

Name	Category	Theorems
`FixedDetMatrix` 📖	CompOp	8 math math: `FixedDetMatrices.reps_zero_empty`, `FixedDetMatrices.reduce_of_pos`, `FixedDetMatrices.T_S_rel_smul`, `FixedDetMatrices.reduce_mem_reps`, `FixedDetMatrices.smul_def`, `FixedDetMatrices.reduce_of_not_pos`, `FixedDetMatrices.smul_coe`, `FixedDetMatrices.S_smul_four`

---

← Back to Index