Documentation Verification Report

JensenFormula

📁 Source: Mathlib/Analysis/Complex/JensenFormula.lean

Statistics

Metric	Count
Definitions	0
Theorems `circleAverage_log_norm`, `circleAverage_log_norm_of_ne_zero`, `sum_divisor_le`, `circleAverage_log_norm`, `circleAverage_log_norm_factorizedRational`, `countingFunction_finsum_eq_finsum_add`	6
Total	6

AnalyticOnNhd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`circleAverage_log_norm` 📖	mathematical	`AnalyticOnNhd` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `Metric.closedBall` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `abs` `Real` `Real.lattice` `Real.instAddGroup`	`Real.circleAverage` `Real` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Real.log` `Norm.norm` `Complex` `Complex.instNorm` `Real.instAdd` `finsum` `Real.instAddCommMonoid` `Real.instMul` `Real.instIntCast` `DFunLike.coe` `Function.locallyFinsuppWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Metric.closedBall` `Complex.instNormedField` `abs` `Real.lattice` `Real.instAddGroup` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Int.instNormedCommRing` `Function.locallyFinsuppWithin.instFunLike` `MeromorphicOn.divisor` `Complex.instNormedAddCommGroup` `Complex.instRCLike` `RCLike.innerProductSpace` `Real.instInv` `Complex.instSub`	—	`MeromorphicOn.circleAverage_log_norm` `meromorphicOn` `MeromorphicOn.AnalyticOnNhd.divisor_apply` `dist_self` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `AnalyticAt.analyticOrderAt_eq_zero` `AnalyticAt.meromorphicTrailingCoeffAt_of_ne_zero` `CharP.cast_eq_zero` `CharP.ofCharZero` `Int.instCharZero` `WithTop.untop₀_zero` `Int.cast_zero` `MulZeroClass.zero_mul` `add_zero`
`circleAverage_log_norm_of_ne_zero` 📖	mathematical	`AnalyticOnNhd` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `Metric.closedBall` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `abs` `Real` `Real.lattice` `Real.instAddGroup`	`Real.circleAverage` `Real` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Real.log` `Norm.norm` `Complex` `Complex.instNorm`	—	`HarmonicOnNhd.circleAverage_eq` `AnalyticAt.harmonicAt_log_norm`
`sum_divisor_le` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `abs` `Real.lattice` `Real.instAddGroup` `Real.instLE` `Real.instOne` `AnalyticOnNhd` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `Metric.closedBall` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Norm.norm` `Complex.instNorm`	`Real` `Real.instLE` `Real.instIntCast` `finsum` `Complex` `Int.instAddCommMonoid` `DFunLike.coe` `Function.locallyFinsuppWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Metric.closedBall` `Complex.instNormedField` `abs` `Real.lattice` `Real.instAddGroup` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Int.instNormedCommRing` `Function.locallyFinsuppWithin.instFunLike` `MeromorphicOn.divisor` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.log` `Norm.norm` `Complex.instNorm`	—	`Eq.le` `map_finsum` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `Function.locallyFinsuppWithin.finiteSupport` `Complex.instT2Space` `ProperSpace.isCompact_closedBall` `Complex.instProperSpace` `abs_div` `Real.instIsStrictOrderedRing` `one_lt_div` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `circleAverage_log_norm` `abs_ne_zero` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Tactic.Ring.atom_pf` `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.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Linarith.lt_of_lt_of_eq` `Mathlib.Tactic.Linarith.add_neg` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `sub_eq_zero_of_eq` `Real.circleAverage_mono_on_of_le_circle` `circleIntegrable_log_norm_meromorphicOn` `meromorphicOn` `mono` `Metric.sphere_subset_closedBall` `eq_zero_or_norm_pos` `norm_zero` `Real.log_zero` `Real.log_nonneg` `Real.log_le_log` `finsum_le_finsum'` `Set.Finite.subset` `Function.support_mul` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `RCLike.charZero_rclike` `MeromorphicOn.AnalyticOnNhd.divisor_apply` `Metric.closedBall_subset_closedBall` `LT.lt.le` `AnalyticAt.analyticOrderAt_eq_zero` `dist_self` `CharP.cast_eq_zero` `CharP.ofCharZero` `Int.instCharZero` `WithTop.untop₀_zero` `Int.cast_zero` `MulZeroClass.zero_mul` `sub_self` `inv_zero` `MulZeroClass.mul_zero` `instReflLe` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `lt_trans` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `Nat.cast_one` `abs_mul` `abs_inv` `abs_norm` `Mathlib.Tactic.FieldSimp.le_eq_cancel_le` `PosMulStrictMono.toPosMulMono` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `LT.lt.ne'` `lt_of_le_of_ne'` `norm_nonneg` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.inv_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.cons_pos` `Real.instZeroLEOneClass` `LT.lt.trans` `zero_lt_one` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `dist_eq_norm'` `Int.instAddLeftMono` `Int.instZeroLEOneClass` `Function.locallyFinsuppWithin.apply_eq_zero_of_notMem` `mul_nonneg` `NeZero.charZero_one` `MeromorphicOn.AnalyticOnNhd.divisor_nonneg` `Real.log_abs` `Mathlib.Tactic.FieldSimp.NF.one_eq_eval` `lt_of_not_ge` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `le_of_not_gt` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Tactic.Linarith.add_lt_of_le_of_neg` `Mathlib.Tactic.Linarith.le_of_eq_of_le` `neg_eq_zero` `Mathlib.Tactic.Linarith.without_one_mul` `Mathlib.Tactic.CancelDenoms.sub_subst` `Mathlib.Tactic.CancelDenoms.add_subst` `Real.log_div` `neg_neg_of_pos` `Mathlib.Tactic.Linarith.zero_lt_one` `norm_ne_zero_iff` `le_div_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.log_pos` `finsum_mul`

MeromorphicOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`circleAverage_log_norm` 📖	mathematical	`MeromorphicOn` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `Metric.closedBall` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `abs` `Real` `Real.lattice` `Real.instAddGroup`	`Real.circleAverage` `Real` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Real.log` `Norm.norm` `Complex` `Complex.instNorm` `Real.instAdd` `finsum` `Real.instAddCommMonoid` `Real.instMul` `Real.instIntCast` `DFunLike.coe` `Function.locallyFinsuppWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Metric.closedBall` `Complex.instNormedField` `abs` `Real.lattice` `Real.instAddGroup` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Int.instNormedCommRing` `Function.locallyFinsuppWithin.instFunLike` `divisor` `Complex.instNormedAddCommGroup` `Complex.instRCLike` `RCLike.innerProductSpace` `Real.instInv` `Complex.instSub` `meromorphicTrailingCoeffAt`	—	`Function.locallyFinsuppWithin.finiteSupport` `Complex.instT2Space` `ProperSpace.isCompact_closedBall` `Complex.instProperSpace` `extract_zeros_poles` `extract_zeros_poles_log` `Real.circleAverage_congr_codiscreteWithin` `Filter.codiscreteWithin.mono` `Metric.sphere_subset_closedBall` `Real.circleAverage_add` `circleIntegrable_log_norm_factorizedRational` `circleIntegrable_log_norm_meromorphicOn` `AnalyticOnNhd.meromorphicOn` `AnalyticOnNhd.mono` `circleAverage_log_norm_factorizedRational` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Real.instIsOrderedCancelAddMonoid` `AnalyticOnNhd.circleAverage_log_norm_of_ne_zero` `dist_self` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `accPt_iff_frequently_nhdsNE` `Filter.compl_notMem` `PerfectSpace.not_isolated` `instPerfectSpace` `mem_nhdsWithin` `Metric.ball_subset_closedBall` `log_norm_meromorphicTrailingCoeffAt_extract_zeros_poles` `add_sub_cancel_left` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_congr` `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.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `finsum_sub_distrib` `Set.Finite.subset` `Function.support_mul` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `RCLike.charZero_rclike` `countingFunction_finsum_eq_finsum_add` `Function.locallyFinsuppWithin.ext` `divisor_apply` `exists_meromorphicOrderAt_ne_top_iff_forall` `Metric.nonempty_closedBall` `abs_nonneg` `Convex.isPreconnected` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `convex_closedBall` `WithTop.untop₀_top` `Function.locallyFinsuppWithin.apply_eq_zero_of_notMem` `Int.cast_zero` `MulZeroClass.zero_mul` `finsum_zero` `add_zero` `zero_add` `MeromorphicAt.meromorphicTrailingCoeffAt_of_order_eq_top` `norm_zero` `Real.log_zero` `Filter.mp_mem` `Filter.self_mem_codiscreteWithin` `meromorphicNFAt_mem_codiscreteWithin` `Filter.univ_mem'` `Int.instIsOrderedAddMonoid` `not_iff_not` `MeromorphicNFAt.meromorphicOrderAt_eq_zero_iff` `mul_inv_rev` `intervalIntegral.integral_zero` `MulZeroClass.mul_zero`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`circleAverage_log_norm_factorizedRational` 📖	mathematical	—	`Real.circleAverage` `Real` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `finsum` `Complex` `Pi.addCommMonoid` `Real.instAddCommMonoid` `Real.instMul` `Real.instIntCast` `DFunLike.coe` `Function.locallyFinsuppWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Metric.closedBall` `abs` `Real.lattice` `Real.instAddGroup` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Int.instNormedCommRing` `Function.locallyFinsuppWithin.instFunLike` `Real.log` `Norm.norm` `Complex.instNorm` `Complex.instSub`	—	`Function.locallyFinsuppWithin.finiteSupport` `Complex.instT2Space` `ProperSpace.isCompact_closedBall` `Complex.instProperSpace` `finsum_eq_sum_of_support_subset` `Mathlib.Tactic.Contrapose.contrapose₁` `Set.Finite.coe_toFinset` `Int.cast_zero` `MulZeroClass.zero_mul` `Real.circleAverage_sum` `IntervalIntegrable.const_mul` `circleIntegrable_log_norm_meromorphicOn` `AnalyticOnNhd.meromorphicOn` `AnalyticOnNhd.sub` `analyticOnNhd_id` `analyticOnNhd_const` `Finset.sum_congr` `Real.circleAverage_fun_smul` `NormedSpace.toNormSMulClass` `Algebra.to_smulCommClass` `circleAverage_log_norm_sub_const_of_mem_closedBall` `Function.locallyFinsuppWithin.supportWithinDomain` `Function.support_mul` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `RCLike.charZero_rclike`
`countingFunction_finsum_eq_finsum_add` 📖	mathematical	—	`finsum` `Real` `Complex` `Real.instAddCommMonoid` `Real.instMul` `Real.instIntCast` `Real.instSub` `Real.log` `Norm.norm` `Complex.instNorm` `Complex.instSub` `Real.instAdd` `Real.instInv`	—	`Function.support_mul` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `RCLike.charZero_rclike` `Set.Finite.coe_toFinset` `finsum_eq_sum_of_support_subset` `Finset.sum_eq_sum_diff_singleton_add` `Set.Finite.mem_toFinset` `sub_self` `norm_zero` `Real.log_zero` `sub_zero` `inv_zero` `MulZeroClass.mul_zero` `add_zero` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Real.instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Finset.sum_congr` `Real.log_mul` `inv_ne_zero` `norm_ne_zero_iff` `Iff.not` `sub_eq_zero` `Real.log_inv` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_congr` `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.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_congr` `Int.cast_zero` `MulZeroClass.zero_mul` `finsum_congr`

---

← Back to Index