Documentation Verification Report

LevelOne

📁 Source: Mathlib/NumberTheory/ModularForms/LevelOne.lean

Statistics

Metric	Count
Definitions	0
Theorems `levelOne_neg_weight_rank_zero`, `levelOne_weight_zero_rank_one`, `levelOne_neg_weight_eq_zero`, `levelOne_weight_zero_const`, `one_mem_strictPeriods_SL2Z`, `exists_one_half_le_im_and_norm_le`, `wt_eq_zero_of_eq_const`	7
Total	7

ModularForm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`levelOne_neg_weight_rank_zero` 📖	mathematical	—	`Module.rank` `Complex` `ModularForm` `Subgroup.map` `Matrix.SpecialLinearGroup` `Fin.fintype` `Int.instCommRing` `Matrix.SpecialLinearGroup.instGroup` `Matrix.GeneralLinearGroup` `Real` `Real.semiring` `Units.instGroup` `Matrix` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `Matrix.SpecialLinearGroup.mapGL` `Real.commRing` `Ring.toIntAlgebra` `Real.instRing` `CongruenceSubgroup.Gamma` `Complex.instSemiring` `AddCommGroup.toAddCommMonoid` `instAddCommGroup` `instModuleComplexOfHasDetOneFinOfNatNatReal` `Subgroup.instHasDetOneMapSpecialLinearGroupGeneralLinearGroupMapGL` `Cardinal` `Cardinal.instZero`	—	`Subgroup.instHasDetOneMapSpecialLinearGroupGeneralLinearGroupMapGL` `rank_eq_zero_iff` `one_ne_zero` `NeZero.charZero_one` `Complex.instCharZero` `one_smul` `ModularFormClass.levelOne_neg_weight_eq_zero` `ModularFormClass.modularForm`
`levelOne_weight_zero_rank_one` 📖	mathematical	—	`Module.rank` `Complex` `ModularForm` `Subgroup.map` `Matrix.SpecialLinearGroup` `Fin.fintype` `Int.instCommRing` `Matrix.SpecialLinearGroup.instGroup` `Matrix.GeneralLinearGroup` `Real` `Real.semiring` `Units.instGroup` `Matrix` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `Matrix.SpecialLinearGroup.mapGL` `Real.commRing` `Ring.toIntAlgebra` `Real.instRing` `CongruenceSubgroup.Gamma` `Complex.instSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `DirectSum.GradeZero.nonUnitalNonAssocSemiring` `AddMonoid.toAddZeroClass` `Int.instAddMonoid` `AddCommGroup.toAddCommMonoid` `instAddCommGroup` `DirectSum.GSemiring.toGNonUnitalNonAssocSemiring` `DirectSum.GRing.toGSemiring` `DirectSum.GCommRing.toGRing` `Int.instAddCommMonoid` `instGCommRing` `Subgroup.instHasDetPlusMinusOneFinOfNatNatRealOfIsArithmetic` `Subgroup.instIsArithmeticMapSpecialLinearGroupFinOfNatNatIntGeneralLinearGroupRealMapGLOfFiniteIndex` `CongruenceSubgroup.instFiniteIndexGamma` `instModuleComplexOfHasDetOneFinOfNatNatReal` `Subgroup.instHasDetOneMapSpecialLinearGroupGeneralLinearGroupMapGL` `Cardinal` `Cardinal.instOne`	—	`rank_eq_one` `Subgroup.instHasDetOneMapSpecialLinearGroupGeneralLinearGroupMapGL` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `Subgroup.instHasDetPlusMinusOneFinOfNatNatRealOfIsArithmetic` `Subgroup.instIsArithmeticMapSpecialLinearGroupFinOfNatNatIntGeneralLinearGroupRealMapGLOfFiniteIndex` `CongruenceSubgroup.instFiniteIndexGamma` `commRing_strongRankCondition` `Complex.instNontrivial` `NeZero.charZero_one` `Complex.instCharZero` `ModularFormClass.levelOne_weight_zero_const` `ModularFormClass.modularForm` `ext` `mul_one`

ModularFormClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`levelOne_neg_weight_eq_zero` 📖	mathematical	—	`DFunLike.coe` `UpperHalfPlane` `Complex` `Pi.instZero` `Complex.instZero`	—	`LT.lt.le` `SlashInvariantForm.wt_eq_zero_of_eq_const` `toSlashInvariantFormClass` `lt_irrefl` `Function.const_zero`
`levelOne_weight_zero_const` 📖	mathematical	—	`DFunLike.coe` `UpperHalfPlane` `Complex`	—	`le_rfl`
`one_mem_strictPeriods_SL2Z` 📖	mathematical	—	`Real` `AddSubgroup` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Real.instRing` `SetLike.instMembership` `AddSubgroup.instSetLike` `Subgroup.strictPeriods` `Subgroup.map` `Matrix.SpecialLinearGroup` `Fin.fintype` `Int.instCommRing` `Matrix.SpecialLinearGroup.instGroup` `Matrix.GeneralLinearGroup` `Real.semiring` `Units.instGroup` `Matrix` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `Matrix.SpecialLinearGroup.mapGL` `Real.commRing` `Ring.toIntAlgebra` `CongruenceSubgroup.Gamma` `Real.instOne`	—	`CongruenceSubgroup.strictPeriods_Gamma` `Nat.cast_one`

SlashInvariantForm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_one_half_le_im_and_norm_le` 📖	mathematical	—	`Real` `Real.instLE` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `UpperHalfPlane.im` `Norm.norm` `Complex` `Complex.instNorm` `DFunLike.coe` `UpperHalfPlane`	—	`Nat.instAtLeastTwoHAddOfNat` `ModularGroup.exists_one_half_le_im_smul_and_norm_denom_le` `slash_action_eqn_SL''` `CongruenceSubgroup.mem_Gamma_one` `norm_mul` `NormedDivisionRing.toNormMulClass` `norm_zpow` `le_mul_of_one_le_left` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `norm_nonneg` `one_le_zpow_of_nonpos₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Real.instZeroLEOneClass` `norm_pos_iff` `UpperHalfPlane.denom_ne_zero`
`wt_eq_zero_of_eq_const` 📖	mathematical	`DFunLike.coe` `UpperHalfPlane` `Complex`	`Complex.instZero`	—	`slash_action_eqn_SL''` `CongruenceSubgroup.mem_Gamma_one` `Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `two_pos` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Complex.ofReal_zpow` `zpow_eq_one_iff_right₀` `IsStrictOrderedRing.toPosMulStrictMono` `LT.lt.le` `Mathlib.Meta.NormNum.isNat_eq_false` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Nat.cast_one` `mul_zpow` `IsCancelMulZero.toIsRightCancelMulZero` `IsDomain.toIsCancelMulZero` `instIsDomain` `ModularGroup.denom_S`

---

← Back to Index