Documentation Verification Report

Discriminant

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

Statistics

Metric	Count
Definitions `discriminant`, `discriminantCuspForm`	2
Theorems `discriminant_S_invariant`, `discriminant_T_invariant`, `discriminant_bounded_factor`, `discriminant_eq_q_prod`, `discriminant_isZeroAtImInfty`, `discriminant_ne_zero`, `eta_comp_eq_csqrt_I_inv`	7
Total	9

ModularForm

Definitions

Name	Category	Theorems
`discriminant` 📖	CompOp	4 math math: `discriminant_isZeroAtImInfty`, `discriminant_eq_q_prod`, `discriminant_T_invariant`, `discriminant_S_invariant`
`discriminantCuspForm` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`discriminant_S_invariant` 📖	mathematical	—	`SlashAction.map` `Matrix.SpecialLinearGroup` `Fin.fintype` `Int.instCommRing` `Matrix.SpecialLinearGroup.monoid` `Pi.addMonoid` `UpperHalfPlane` `Complex` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Complex.instNormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SLAction` `ModularGroup.S` `discriminant`	—	`neg_div` `one_div` `eta_comp_eq_csqrt_I_inv` `UpperHalfPlane.coe_im_pos` `mul_pow` `inv_pow` `UpperHalfPlane.ne_zero` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.inv_eq_eval` `Mathlib.Tactic.FieldSimp.NF.one_eq_eval` `Mathlib.Tactic.FieldSimp.NF.pow_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `one_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_ofNat` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `SL_slash_apply` `UpperHalfPlane.im_inv_neg_coe_pos` `UpperHalfPlane.modular_S_smul` `inv_neg` `Matrix.cons_val'` `Matrix.cons_val_fin_one` `Int.cast_one` `Int.cast_zero` `add_zero` `zpow_neg`
`discriminant_T_invariant` 📖	mathematical	—	`SlashAction.map` `Matrix.SpecialLinearGroup` `Fin.fintype` `Int.instCommRing` `Matrix.SpecialLinearGroup.monoid` `Pi.addMonoid` `UpperHalfPlane` `Complex` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Complex.instNormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SLAction` `ModularGroup.T` `discriminant`	—	`SL_slash_apply` `UpperHalfPlane.denom.eq_1` `UpperHalfPlane.modular_T_smul` `ModularGroup.T.eq_1` `Nat.instAtLeastTwoHAddOfNat` `discriminant_eq_q_prod` `div_one` `Matrix.cons_val'` `Matrix.cons_val_fin_one` `Int.cast_zero` `MulZeroClass.zero_mul` `Int.cast_one` `zero_add` `zpow_neg` `one_zpow` `inv_one` `mul_one` `Complex.exp_periodic` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf'` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.add_congr` `Nat.cast_one` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.RingNF.add_assoc_rev` `Mathlib.Tactic.RingNF.mul_assoc_rev` `Mathlib.Tactic.RingNF.nat_rawCast_1` `pow_one` `add_zero` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.pow_one_cast` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `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.pow_nat` `Mathlib.Tactic.Ring.coeff_one` `Mathlib.Tactic.Ring.pow_bit0` `Mathlib.Tactic.Ring.pow_bit1` `Mathlib.Tactic.Ring.pow_one` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Tactic.RingNF.int_rawCast_neg` `Mathlib.Tactic.RingNF.mul_neg` `Mathlib.Tactic.RingNF.add_neg`
`discriminant_bounded_factor` 📖	mathematical	—	`Filter.Tendsto` `UpperHalfPlane` `Complex` `tprod` `CommRing.toCommMonoid` `Complex.commRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `CommCStarAlgebra.toNormedCommRing` `instCommCStarAlgebraComplex` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Complex.instSub` `Complex.instOne` `eta_q` `UpperHalfPlane.coe` `SummationFilter.unconditional` `UpperHalfPlane.atImInfty` `nhds`	—	`Nat.instAtLeastTwoHAddOfNat` `tendsto_tprod_one_add_of_dominated_convergence` `NormedDivisionRing.to_normOneClass` `Complex.instCompleteSpace` `sub_eq_add_neg` `norm_neg` `norm_pow` `NormedDivisionRing.toNormMulClass` `add_zero` `tprod_one` `pow_succ'` `Summable.mul_left` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `summable_geometric_of_abs_lt_one` `Mathlib.Meta.NormNum.isNNRat_lt_true` `Real.instIsStrictOrderedRing` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero` `Mathlib.Meta.NormNum.isNNRat_abs_nonneg` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.instAtLeastTwo` `zero_pow` `neg_zero` `Filter.Tendsto.neg` `IsSemitopologicalRing.toContinuousNeg` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Continuous.tendsto` `continuous_pow` `IsTopologicalSemiring.toContinuousMul` `Filter.mp_mem` `Metric.ball_mem_nhds` `Nat.cast_zero` `Filter.univ_mem'` `pow_le_pow_left₀` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `IsOrderedRing.toMulPosMono` `norm_nonneg` `LT.lt.le` `mem_ball_zero_iff` `Filter.Tendsto.pow` `Filter.Tendsto.comp` `UpperHalfPlane.qParam_tendsto_atImInfty` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `div_one` `Multipliable.tprod_pow` `Complex.instT2Space` `SummationFilter.instNeBotUnconditional` `Multipliable.congr` `MultipliableLocallyUniformlyOn.multipliable` `multipliableLocallyUniformlyOn_eta` `UpperHalfPlane.coe_im_pos` `Nat.cast_add` `one_pow`
`discriminant_eq_q_prod` 📖	mathematical	—	`discriminant` `Complex` `Complex.instMul` `Function.Periodic.qParam` `Real` `Real.instOne` `UpperHalfPlane.coe` `tprod` `CommRing.toCommMonoid` `Complex.commRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `CommCStarAlgebra.toNormedCommRing` `instCommCStarAlgebraComplex` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Complex.instSub` `Complex.instOne` `eta_q` `SummationFilter.unconditional`	—	`mul_pow` `Nat.instAtLeastTwoHAddOfNat` `nsmul_eq_mul` `div_one` `Multipliable.tprod_pow` `Complex.instT2Space` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SummationFilter.instNeBotUnconditional` `MultipliableLocallyUniformlyOn.multipliable` `multipliableLocallyUniformlyOn_eta` `UpperHalfPlane.coe_im_pos`
`discriminant_isZeroAtImInfty` 📖	mathematical	—	`UpperHalfPlane.IsZeroAtImInfty` `Complex` `Complex.instZero` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `CommCStarAlgebra.toNormedCommRing` `instCommCStarAlgebraComplex` `discriminant`	—	`Filter.Tendsto.congr` `discriminant_eq_q_prod` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Nat.cast_one` `Mathlib.Tactic.Ring.zero_mul` `Filter.Tendsto.mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `UpperHalfPlane.qParam_tendsto_atImInfty` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `discriminant_bounded_factor`
`discriminant_ne_zero` 📖	—	—	—	—	`isReduced_of_noZeroDivisors` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `eta_ne_zero` `UpperHalfPlane.coe_im_pos`
`eta_comp_eq_csqrt_I_inv` 📖	mathematical	—	`Set.EqOn` `Complex` `eta` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `Complex.instNeg` `Complex.instOne` `Function.hasSMul` `Algebra.toSMul` `Complex.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Complex.instInv` `Complex.sqrt` `Complex.I` `Pi.instMul` `Complex.instMul` `UpperHalfPlane.upperHalfPlaneSet`	—	`Complex.div_I` `neg_mul` `one_mul` `neg_neg` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike`

---

← Back to Index