Manifold

📁 Source: Mathlib/Analysis/Complex/UpperHalfPlane/Manifold.lean

Statistics

Metric	Count
Definitions instChartedSpaceComplex	1
Theorems contMDiffAt_iff, contMDiffAt_ofComplex, contMDiff_coe, contMDiff_denom, contMDiff_denom_zpow, contMDiff_inv_denom, contMDiff_num, contMDiff_smul, eq_zero_of_frequently, instIsManifoldComplexModelWithCornersSelfTopWithTopENat, mdifferentiableAt_iff, mdifferentiableAt_ofComplex, mdifferentiable_coe, mdifferentiable_denom, mdifferentiable_denom_zpow, mdifferentiable_iff, mdifferentiable_inv_denom, mdifferentiable_num, mdifferentiable_smul, mul_eq_zero_iff, prod_eq_zero_iff	21
Total	22

UpperHalfPlane

Definitions

Name	Category	Theorems
instChartedSpaceComplex 📖	CompOp	25 math math: mdifferentiable_num, CuspFormClass.holo, mdifferentiable_inv_denom, contMDiff_coe, CuspForm.holo', contMDiff_inv_denom, contMDiff_num, mdifferentiable_denom, contMDiff_denom_zpow, mdifferentiable_jacobiTheta, contMDiffAt_ofComplex, ModularForm.holo', contMDiffAt_iff, instIsManifoldComplexModelWithCornersSelfTopWithTopENat, mdifferentiable_coe, ModularFormClass.holo, EisensteinSeries.eisensteinSeries_SIF_MDifferentiable, mdifferentiableAt_iff, contMDiff_smul, contMDiff_denom, EisensteinSeries.eisensteinSeriesSIF_mdifferentiable, mdifferentiable_denom_zpow, mdifferentiable_iff, mdifferentiableAt_ofComplex, mdifferentiable_smul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contMDiffAt_iff 📖	mathematical	—	ContMDiffAt Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace modelWithCornersSelf UpperHalfPlane instTopologicalSpace instChartedSpaceComplex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField chartedSpaceSelf ContDiffAt OpenPartialHomeomorph.toFun' ofComplex coe	—	contMDiffAt_iff_contDiffAt ContMDiffAt.comp ofComplex_apply contMDiffAt_ofComplex im_pos contMDiff_coe
contMDiffAt_ofComplex 📖	mathematical	Real Real.instLT Real.instZero Complex.im	ContMDiffAt Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace modelWithCornersSelf SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField chartedSpaceSelf UpperHalfPlane instTopologicalSpace instChartedSpaceComplex OpenPartialHomeomorph.toFun' ofComplex	—	contMDiffAt_iff ContinuousAt.eq_1 nhds_induced Filter.tendsto_comap_iff Filter.Tendsto.congr' Filter.EventuallyEq.symm eventuallyEq_coe_comp_ofComplex ofComplex_apply_of_im_pos Filter.tendsto_id isOpenEmbedding_coe PartialEquiv.trans_refl CompTriple.comp_eq CompTriple.instComp_id CompTriple.instIsIdId Set.range_id ContDiffAt.congr_of_eventuallyEq contDiffAt_id
contMDiff_coe 📖	mathematical	—	ContMDiff Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace modelWithCornersSelf UpperHalfPlane instTopologicalSpace instChartedSpaceComplex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField chartedSpaceSelf coe	—	contMDiffAt_extChartAt
contMDiff_denom 📖	mathematical	—	ContMDiff Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace modelWithCornersSelf UpperHalfPlane instTopologicalSpace instChartedSpaceComplex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField chartedSpaceSelf denom coe	—	ContMDiff.add instContMDiffAddSelf ContMDiff.smul contMDiff_const contMDiff_coe
contMDiff_denom_zpow 📖	mathematical	—	ContMDiff Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace modelWithCornersSelf UpperHalfPlane instTopologicalSpace instChartedSpaceComplex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField chartedSpaceSelf DivInvMonoid.toZPow Complex.instDivInvMonoid denom coe	—	DifferentiableOn.analyticOnNhd Complex.instCompleteSpace differentiableOn_zpow isOpen_compl_singleton T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace denom_ne_zero ContMDiffAt.comp ContDiffAt.contMDiffAt AnalyticAt.contDiffAt contMDiff_denom
contMDiff_inv_denom 📖	mathematical	—	ContMDiff Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace modelWithCornersSelf UpperHalfPlane instTopologicalSpace instChartedSpaceComplex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField chartedSpaceSelf Complex.instInv denom coe	—	zpow_neg zpow_one contMDiff_denom_zpow
contMDiff_num 📖	mathematical	—	ContMDiff Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace modelWithCornersSelf UpperHalfPlane instTopologicalSpace instChartedSpaceComplex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField chartedSpaceSelf num coe	—	ContMDiff.add instContMDiffAddSelf ContMDiff.smul contMDiff_const contMDiff_coe
contMDiff_smul 📖	mathematical	Real Real.instLT Real.instZero Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing DFunLike.coe MonoidHom Matrix.GeneralLinearGroup Fin.fintype Units MulOneClass.toMulOne Units.instMulOneClass Matrix Matrix.semiring MonoidHom.instFunLike Matrix.GeneralLinearGroup.det	ContMDiff Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace modelWithCornersSelf UpperHalfPlane instTopologicalSpace instChartedSpaceComplex Real.semiring SemigroupAction.toSMul Monoid.toSemigroup Units.instMonoid MulAction.toSemigroupAction glAction	—	contMDiffAt_iff_target Continuous.continuousAt ContinuousConstSMul.continuous_const_smul instContinuousGLSMul im_pos coe_smul_of_det_pos isOpenEmbedding_coe glPos_smul_def PartialEquiv.trans_refl ContMDiffAt.mul instContMDiffMulOfTopWithTopENat ContMDiffRing.toContMDiffMul instFieldContMDiffRing contMDiff_num contMDiff_inv_denom
eq_zero_of_frequently 📖	mathematical	MDifferentiable Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace modelWithCornersSelf UpperHalfPlane instTopologicalSpace instChartedSpaceComplex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField chartedSpaceSelf Filter.Frequently Complex.instZero nhdsWithin Compl.compl Set Set.instCompl Set.instSingletonSet	Pi.instZero	—	DifferentiableOn.analyticOnNhd Complex.instCompleteSpace mdifferentiable_iff isOpen_upperHalfPlaneSet ofComplex_apply AnalyticOnNhd.eqOn_zero_of_preconnected_of_frequently_eq_zero IsConnected.isPreconnected Complex.isConnected_of_upperHalfPlane subset_rfl Set.instReflSubset coe_im_pos Mathlib.Tactic.Contrapose.contrapose₁ eventually_nhdsWithin_iff Filter.mp_mem Filter.eventually_map Topology.IsOpenEmbedding.map_nhds_eq isOpenEmbedding_coe Filter.univ_mem' im_pos
instIsManifoldComplexModelWithCornersSelfTopWithTopENat 📖	mathematical	—	IsManifold Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace modelWithCornersSelf Top.top WithTop ENat WithTop.top UpperHalfPlane instTopologicalSpace instChartedSpaceComplex	—	Topology.IsOpenEmbedding.isManifold_singleton isOpenEmbedding_coe
mdifferentiableAt_iff 📖	mathematical	—	MDifferentiableAt Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace modelWithCornersSelf UpperHalfPlane instTopologicalSpace instChartedSpaceComplex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField chartedSpaceSelf DifferentiableAt Complex.addCommGroup Complex.instModuleSelf OpenPartialHomeomorph.toFun' ofComplex coe	—	mdifferentiableAt_iff_differentiableAt MDifferentiableAt.comp ofComplex_apply mdifferentiableAt_ofComplex im_pos mdifferentiable_coe
mdifferentiableAt_ofComplex 📖	mathematical	Real Real.instLT Real.instZero Complex.im	MDifferentiableAt Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace modelWithCornersSelf SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField chartedSpaceSelf UpperHalfPlane instTopologicalSpace instChartedSpaceComplex OpenPartialHomeomorph.toFun' ofComplex	—	ContMDiffAt.mdifferentiableAt contMDiffAt_ofComplex one_ne_zero NeZero.charZero_one WithTop.charZero
mdifferentiable_coe 📖	mathematical	—	MDifferentiable Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace modelWithCornersSelf UpperHalfPlane instTopologicalSpace instChartedSpaceComplex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField chartedSpaceSelf coe	—	ContMDiff.mdifferentiable contMDiff_coe one_ne_zero NeZero.charZero_one WithTop.charZero
mdifferentiable_denom 📖	mathematical	—	MDifferentiable Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace modelWithCornersSelf UpperHalfPlane instTopologicalSpace instChartedSpaceComplex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField chartedSpaceSelf denom coe	—	ContMDiff.mdifferentiable contMDiff_denom one_ne_zero NeZero.charZero_one WithTop.charZero
mdifferentiable_denom_zpow 📖	mathematical	—	MDifferentiable Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace modelWithCornersSelf UpperHalfPlane instTopologicalSpace instChartedSpaceComplex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField chartedSpaceSelf DivInvMonoid.toZPow Complex.instDivInvMonoid denom coe	—	ContMDiff.mdifferentiable contMDiff_denom_zpow one_ne_zero NeZero.charZero_one WithTop.charZero
mdifferentiable_iff 📖	mathematical	—	MDifferentiable Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace modelWithCornersSelf UpperHalfPlane instTopologicalSpace instChartedSpaceComplex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField chartedSpaceSelf DifferentiableOn Complex.addCommGroup Complex.instModuleSelf OpenPartialHomeomorph.toFun' ofComplex setOf Real Real.instLT Real.instZero Complex.im	—	DifferentiableAt.differentiableWithinAt mdifferentiableAt_iff DifferentiableWithinAt.differentiableAt IsOpen.mem_nhds isOpen_upperHalfPlaneSet
mdifferentiable_inv_denom 📖	mathematical	—	MDifferentiable Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace modelWithCornersSelf UpperHalfPlane instTopologicalSpace instChartedSpaceComplex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField chartedSpaceSelf Complex.instInv denom coe	—	ContMDiff.mdifferentiable contMDiff_inv_denom one_ne_zero NeZero.charZero_one WithTop.charZero
mdifferentiable_num 📖	mathematical	—	MDifferentiable Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace modelWithCornersSelf UpperHalfPlane instTopologicalSpace instChartedSpaceComplex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField chartedSpaceSelf num coe	—	ContMDiff.mdifferentiable contMDiff_num one_ne_zero NeZero.charZero_one WithTop.charZero
mdifferentiable_smul 📖	mathematical	Real Real.instLT Real.instZero Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing DFunLike.coe MonoidHom Matrix.GeneralLinearGroup Fin.fintype Units MulOneClass.toMulOne Units.instMulOneClass Matrix Matrix.semiring MonoidHom.instFunLike Matrix.GeneralLinearGroup.det	MDifferentiable Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace modelWithCornersSelf UpperHalfPlane instTopologicalSpace instChartedSpaceComplex Real.semiring SemigroupAction.toSMul Monoid.toSemigroup Units.instMonoid MulAction.toSemigroupAction glAction	—	ContMDiff.mdifferentiable contMDiff_smul one_ne_zero NeZero.charZero_one WithTop.charZero
mul_eq_zero_iff 📖	mathematical	MDifferentiable Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace modelWithCornersSelf UpperHalfPlane instTopologicalSpace instChartedSpaceComplex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField chartedSpaceSelf	Pi.instMul Complex.instMul Pi.instZero Complex.instZero	—	eq_zero_of_frequently Filter.frequently_or_distrib Filter.Frequently.of_forall PerfectSpace.not_isolated instPerfectSpaceOfT1SpaceOfConnectedSpaceOfNontrivial T4Space.toT1Space instT4Space PathConnectedSpace.connectedSpace ContractibleSpace.instPathConnectedSpace instContractibleSpace instNontrivial NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass
prod_eq_zero_iff 📖	mathematical	MDifferentiable Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace modelWithCornersSelf UpperHalfPlane instTopologicalSpace instChartedSpaceComplex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField chartedSpaceSelf	Finset.prod Pi.commMonoid CommRing.toCommMonoid Complex.commRing Pi.instZero Complex.instZero Finset Finset.instMembership	—	Filter.Frequently.of_forall PerfectSpace.not_isolated instPerfectSpaceOfT1SpaceOfConnectedSpaceOfNontrivial T4Space.toT1Space instT4Space PathConnectedSpace.connectedSpace ContractibleSpace.instPathConnectedSpace instContractibleSpace instNontrivial Finset.prod_apply eq_zero_of_frequently Complex.instNontrivial NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Finset.prod_eq_zero

---

← Back to Index