Documentation Verification Report

NormTrace

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

Statistics

Metric	Count
Definitions `norm`, `norm`, `quotientFunc`, `instMulActionSubtypeGeneralLinearGroupFinOfNatNatRealMemSubgroup`, `instMulActionSubtypeGeneralLinearGroupFinOfNatNatRealMemSubgroupQuotientSubgroupOf`	5
Theorems `coe_trace`, `coe_norm`, `coe_trace`, `eq_const_of_weight_zero`, `isZero_of_neg_weight`, `norm_eq_zero_iff`, `norm_ne_zero`, `coe_norm`, `coe_trace`, `quotientFunc_mk`, `quotientFunc_smul`	11
Total	16

CuspForm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_trace` 📖	mathematical	—	`DFunLike.coe` `CuspForm` `UpperHalfPlane` `Complex` `funLike` `trace` `Finset.sum` `HasQuotient.Quotient` `Matrix.GeneralLinearGroup` `Real` `Fin.fintype` `Real.semiring` `Subgroup` `Units.instGroup` `Matrix` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.toGroup` `QuotientGroup.instHasQuotientSubgroup` `Subgroup.subgroupOf` `Pi.addCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `Finset.univ` `Fintype.ofFinite` `SlashInvariantForm.quotientFunc` `ModularFormClass.toSlashInvariantFormClass` `instModularFormClassOfCuspFormClass`	—	—

ModularForm

Definitions

Name	Category	Theorems
`norm` 📖	CompOp	2 math math: `norm_eq_zero_iff`, `coe_norm`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_norm` 📖	mathematical	—	`DFunLike.coe` `ModularForm` `Nat.card` `HasQuotient.Quotient` `Matrix.GeneralLinearGroup` `Real` `Fin.fintype` `Real.semiring` `Subgroup` `Units.instGroup` `Matrix` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.toGroup` `QuotientGroup.instHasQuotientSubgroup` `Subgroup.subgroupOf` `UpperHalfPlane` `Complex` `funLike` `norm` `Finset.prod` `Pi.commMonoid` `CommRing.toCommMonoid` `Complex.commRing` `Finset.univ` `Fintype.ofFinite` `SlashInvariantForm.quotientFunc` `ModularFormClass.toSlashInvariantFormClass`	—	—
`coe_trace` 📖	mathematical	—	`DFunLike.coe` `ModularForm` `UpperHalfPlane` `Complex` `funLike` `trace` `Finset.sum` `HasQuotient.Quotient` `Matrix.GeneralLinearGroup` `Real` `Fin.fintype` `Real.semiring` `Subgroup` `Units.instGroup` `Matrix` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.toGroup` `QuotientGroup.instHasQuotientSubgroup` `Subgroup.subgroupOf` `Pi.addCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `Finset.univ` `Fintype.ofFinite` `SlashInvariantForm.quotientFunc` `ModularFormClass.toSlashInvariantFormClass`	—	—
`eq_const_of_weight_zero` 📖	mathematical	—	`DFunLike.coe` `ModularForm` `UpperHalfPlane` `Complex` `funLike`	—	`Subgroup.IsArithmetic.inter` `Subgroup.instIsArithmeticRangeSpecialLinearGroupFinOfNatNatIntGeneralLinearGroupRealMapGL` `Subgroup.instHasDetOneMinGeneralLinearGroup_1` `Subgroup.instHasDetOneRangeSpecialLinearGroupGeneralLinearGroupMapGL` `SlashInvariantForm.slash_action_eq'` `holo'` `bdd_at_cusps'` `IsCusp.mono` `inf_le_left`
`isZero_of_neg_weight` 📖	mathematical	—	`ModularForm` `instZero`	—	`Subgroup.IsArithmetic.isFiniteRelIndexSL` `Subgroup.instHasDetPlusMinusOneFinOfNatNatRealOfIsArithmetic` `Subgroup.instIsArithmeticRangeSpecialLinearGroupFinOfNatNatIntGeneralLinearGroupRealMapGL` `ModularFormClass.modularForm` `ext` `ModularFormClass.levelOne_neg_weight_eq_zero` `CongruenceSubgroup.Gamma_one_top` `MonoidHom.range_eq_map` `mul_neg_of_neg_of_pos` `IsStrictOrderedRing.toMulPosStrictMono` `Int.instIsStrictOrderedRing` `Nat.cast_zero` `Int.instAddLeftMono` `Int.instZeroLEOneClass` `Int.instCharZero` `Subgroup.relIndex_ne_zero` `Pi.zero_apply` `zero_apply`
`norm_eq_zero_iff` 📖	mathematical	—	`norm` `ModularForm` `Nat.card` `HasQuotient.Quotient` `Matrix.GeneralLinearGroup` `Real` `Fin.fintype` `Real.semiring` `Subgroup` `Units.instGroup` `Matrix` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.toGroup` `QuotientGroup.instHasQuotientSubgroup` `Subgroup.subgroupOf` `instZero` `DFunLike.coe` `UpperHalfPlane` `Complex` `Pi.instZero` `Complex.instZero`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `norm_ne_zero` `ext` `ModularFormClass.toSlashInvariantFormClass` `Finset.prod_apply` `Complex.instNontrivial` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `SubmonoidClass.toOneMemClass` `SubgroupClass.toSubmonoidClass` `Subgroup.instSubgroupClass` `inv_one` `SlashAction.slash_one`
`norm_ne_zero` 📖	—	—	—	—	`Mathlib.Tactic.Contrapose.contrapose₄` `ModularFormClass.toSlashInvariantFormClass` `One.instNonempty` `UpperHalfPlane.prod_eq_zero_iff` `Quotient.forall` `holo'` `coe_zero` `coe_norm` `DFunLike.coe_injective`

SlashInvariantForm

Definitions

Name	Category	Theorems
`norm` 📖	CompOp	1 math math: `coe_norm`
`quotientFunc` 📖	CompOp	7 math math: `quotientFunc_mk`, `quotientFunc_smul`, `CuspForm.coe_trace`, `coe_trace`, `ModularForm.coe_norm`, `ModularForm.coe_trace`, `coe_norm`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_norm` 📖	mathematical	—	`DFunLike.coe` `SlashInvariantForm` `Nat.card` `HasQuotient.Quotient` `Matrix.GeneralLinearGroup` `Real` `Fin.fintype` `Real.semiring` `Subgroup` `Units.instGroup` `Matrix` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.toGroup` `QuotientGroup.instHasQuotientSubgroup` `Subgroup.subgroupOf` `UpperHalfPlane` `Complex` `funLike` `norm` `Finset.prod` `Pi.commMonoid` `CommRing.toCommMonoid` `Complex.commRing` `Finset.univ` `Fintype.ofFinite` `quotientFunc`	—	—
`coe_trace` 📖	mathematical	—	`DFunLike.coe` `SlashInvariantForm` `UpperHalfPlane` `Complex` `funLike` `trace` `Finset.sum` `HasQuotient.Quotient` `Matrix.GeneralLinearGroup` `Real` `Fin.fintype` `Real.semiring` `Subgroup` `Units.instGroup` `Matrix` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.toGroup` `QuotientGroup.instHasQuotientSubgroup` `Subgroup.subgroupOf` `Pi.addCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `Finset.univ` `Fintype.ofFinite` `quotientFunc`	—	—
`quotientFunc_mk` 📖	mathematical	—	`quotientFunc` `Matrix.GeneralLinearGroup` `Real` `Fin.fintype` `Real.semiring` `Subgroup` `Units.instGroup` `Matrix` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `SetLike.instMembership` `Subgroup.instSetLike` `QuotientGroup.leftRel` `Subgroup.toGroup` `Subgroup.subgroupOf` `SlashAction.map` `Units.instMonoid` `Pi.addMonoid` `UpperHalfPlane` `Complex` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Complex.instNormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ModularForm.instSlashActionIntGeneralLinearGroupFinOfNatNatRealForallUpperHalfPlaneComplex` `Units.instInv` `DFunLike.coe`	—	—
`quotientFunc_smul` 📖	mathematical	`Matrix.GeneralLinearGroup` `Real` `Fin.fintype` `Real.semiring` `Subgroup` `Units.instGroup` `Matrix` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `SetLike.instMembership` `Subgroup.instSetLike`	`SlashAction.map` `Units.instMonoid` `Pi.addMonoid` `UpperHalfPlane` `Complex` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Complex.instNormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ModularForm.instSlashActionIntGeneralLinearGroupFinOfNatNatRealForallUpperHalfPlaneComplex` `quotientFunc` `HasQuotient.Quotient` `Subgroup.toGroup` `QuotientGroup.instHasQuotientSubgroup` `Subgroup.subgroupOf` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `instMulActionSubtypeGeneralLinearGroupFinOfNatNatRealMemSubgroupQuotientSubgroupOf` `Subgroup.inv`	—	`mul_inv_rev` `inv_inv` `SlashAction.slash_mul`

(root)

Definitions

Name	Category	Theorems
`instMulActionSubtypeGeneralLinearGroupFinOfNatNatRealMemSubgroup` 📖	CompOp	—
`instMulActionSubtypeGeneralLinearGroupFinOfNatNatRealMemSubgroupQuotientSubgroupOf` 📖	CompOp	1 math math: `SlashInvariantForm.quotientFunc_smul`

---

← Back to Index