| Q204 | 0 | zero_add, MulZeroClass.mul_zero, Nat.zero_le, Nat.succ_ne_zero, Even.zero, Ideal.isPrime_bot, add_zero, sub_zero, inv_zero, pow_zero, Finset.prod_empty, Nat.factorial_zero, Cardinal.mk_eq_zero, Ordinal.bot_eq_zero, Zero, Pi.zero_apply, CategoryTheory.Limits.IsZero, zero_div, neg_zero, zero_pow, CategoryTheory.Limits.HasZeroMorphisms, dvd_zero, Rat.cast_zero, isAlgebraic_rat, MulZeroClass, deriv.lhopital_zero_atTop |
| Q199 | 1 | Nat.succ, one_mul, one_pow, MulOneClass, IsUnit, Nat.factorial_one, Finset.prod_empty, unitInterval, MeasureTheory.IsProbabilityMeasure |
| Q37413 | 100 | Nat |
| Q200 | 2 | Nat.succ, Nat.Prime.even_iff, even_iff_two_dvd, ZMod.instField, ZMod.intCast_zmod_eq_zero_iff_dvd, CharTwo.add_self_eq_zero, Function.Involutive |
| Q201 | 3 | Nat.three_dvd_iff, Nat.dvd_iff_dvd_digits_sum, Affine.Triangle |
| Q202 | 4 | Nat.sum_four_squares, IsKleinFour |
| Q23488 | 6 | Nat |
| Q23350 | 7 | Nat |
| Q19108 | 9 | Nat.nine_dvd_iff |
| Q318737 | Abelian category | CategoryTheory.Abelian, AddCommGrpCat.instAbelian, CategoryTheory.Preadditive, ModuleCat.abelian, CategoryTheory.Abelian.freyd_mitchell, CategoryTheory.sheafIsAbelian, CategoryTheory.Abelian.functorCategoryAbelian, CategoryTheory.HasExactColimitsOfShape, CategoryTheory.Limits.HasProducts, CategoryTheory.HasExactLimitsOfShape, CategoryTheory.Limits.HasZeroMorphisms, CategoryTheory.Abelian.imageStrongEpiMonoFactorisation, CategoryTheory.Subobject.boundedOrder, CategoryTheory.ShortComplex.SnakeInput.snake_lemma, MonoidAlgebra.Submodule.exists_isCompl, CategoryTheory.ObjectProperty.IsSerreClass |
| Q181296 | Abelian group | CommGroup, PUnit.commGroup, Int.instAddCommGroup, IsCyclic.commGroup, NonUnitalNonAssocRing, Units.instCommGroupUnits, Subgroup.normal_of_isMulCommutative, Subgroup.toCommGroup, CommGroup.is_simple_iff_prime_card, ModuleCat.forget₂AddCommGroupIsEquivalence, AddCommGroup.toIntModule, AddCommGroup.equiv_free_prod_directSum_zmod, AddMonoidHom.add, Module.rank, rank_eq_zero_iff_isTorsion, Subgroup.center, Subgroup.center_eq_top_iff, commGroupOfCyclicCenterQuotient, AddCommGroup.equiv_directSum_zmod_of_finite, isCyclic_of_prime_card, IsPGroup.commutative_of_card_eq_prime_sq, ZMod.chineseRemainder, AddGroup.FG, FreeAbelianGroup.lift, Module.Basis.SmithNormalForm, instIsAddCyclicInt, DivisibleBy, Monoid.IsTorsion, IsMulTorsionFree, Submodule.instIsTorsionFree, AddCommGrpCat.instAbelian, AddGroup |
| Q318751 | Abelian variety | AlgebraicGeometry.isCommMonObj_of_isProper_of_geometricallyIntegral |
| Q120812 | Absolute value | abs_of_nonneg, abs_nonneg, Real.dist_0_eq_abs, Real.sqrt_sq_eq_abs, AbsoluteValue.abs, abs_abs, abs_le, Real.dist_eq, Complex.norm_def, Complex.norm_mul_cos_add_sin_mul_I, Complex.normSq_eq_norm_sq, Complex.norm_mul, Continuous.abs, not_differentiableAt_abs_zero, abs_neg, self_mul_sign, sup_eq_half_smul_add_add_abs_sub, max_sub_min_eq_abs, hasDerivAt_abs, HasFDerivAt.abs, hasDerivAt_abs_rpow, EuclideanSpace.dist_eq, PseudoMetricSpace, abs_eq_max_neg, AbsoluteValue, AbsoluteValue.map_one, IsNonarchimedean, NormedSpace, Norm, EuclideanSpace.norm_eq, norm_eq_sqrt_real_inner |
| Q159943 | Abstract algebra | Real.sqrt_mul, Monoid, Sylow.exists_subgroup_card_pow_prime, Equiv.Perm.subgroupOfMulAction, CompositionSeries.jordan_holder, Algebra, Ideal.uniqueFactorizationMonoid, Submodule.isLasker, Polynomial.isNoetherianRing, Ring, Field, IntermediateField, MagmaCat, Semigroup, Group |
| Q272035 | Accuracy and precision | ProbabilityTheory.tendstoInDistribution_inv_sqrt_mul_sum_sub |
| Q32043 | Addition | HAdd.hAdd, add_comm, add_assoc, Nat.succ_eq_add_one, add_zero, Finset.sum, tsum, Cardinal.add_def, Nat.add_succ, Int.lt_add_one_iff, Nat.add, Nat.add_assoc, Int.add, Rat.add, add_div, Real.instAdd, Real.instNeg, Complex.add_re, AddCommGroup, Pi.instAdd, Matrix.add_apply, ZMod, Real.Angle, AddCommSemigroup, AddCommMonoid, Finsupp.linearCombination, Ordinal.add, Cardinal.commSemiring, CategoryTheory.Limits.coprod, DirectSum, sub_eq_add_neg, AddMonoid.nsmul_succ, Real.exp_add, Distrib, Cardinal.add_eq_max, max_add_add_left, Tropical, AddGroup, zero_add, xor |
| Q357858 | Adjoint functors | CategoryTheory.Adjunction, CategoryTheory.Functor.IsLeftAdjoint, CategoryTheory.Equivalence.toAdjunction, CategoryTheory.Adjunction.homEquiv, CategoryTheory.leftAdjointOfStructuredArrowInitials, CategoryTheory.rightAdjointOfCostructuredArrowTerminals, CategoryTheory.Adjunction.isRightAdjoint, CategoryTheory.Adjunction.mkOfHomEquiv, CategoryTheory.Adjunction.left_triangle, CategoryTheory.ihom.adjunction, GrpCat.adj, CategoryTheory.Limits.constLimAdj, CategoryTheory.Limits.colimConstAdj, MonCat.adjoinOneAdj, ModuleCat.extendRestrictScalarsAdj, ModuleCat.restrictCoextendScalarsAdj, GrpCat.abelianizeAdj, Rep.indResAdjunction, TopCat.adj₁, TopCat.Sheaf.pullbackPushforwardAdjunction, GaloisConnection, GaloisConnection.closureOperator, Set.image_preimage, CategoryTheory.Adjunction.CoreHomEquivUnitCounit, CategoryTheory.Adjunction.adjunctionOfEquivLeft, CategoryTheory.isRightAdjoint_of_preservesLimits_of_solutionSetCondition, CategoryTheory.Adjunction.rightAdjointUniq, CategoryTheory.Adjunction.ofNatIsoRight, CategoryTheory.Adjunction.comp, CategoryTheory.Adjunction.rightAdjoint_preservesLimits, CategoryTheory.Adjunction.right_adjoint_additive, CategoryTheory.adjunctionOfStructuredArrowInitials, CategoryTheory.Equivalence.isLeftAdjoint_functor, CategoryTheory.Adjunction.toMonad, CategoryTheory.Adjunction.adjToMonadIso, CategoryTheory.Adjunction.unit, CategoryTheory.Monad.adj, MonCat.adj |
| Q1017106 | Adjoint representation | LieAlgebra.ad, LieRing.ofAssociativeRing, LieDerivation.ad_ker_eq_center, LieAlgebra.ad_lie, LieAlgebra.ad_pow_lie, LieAlgebra.IsKilling.rootSystem, lie_lie |
| Q382520 | Affine geometry | AffineMap, AddTorsor, AffineSubspace.Parallel.equivalence, Finset.affineCombination |
| Q382698 | Affine space | AddTorsor, AffineSubspace.mk', Finset.affineCombination, AddAction, eq_vadd_iff_vsub_eq, vsub_vadd, AffineSubspace, AffineSubspace.mk'_eq, AffineSubspace.direction, AffineSubspace.Parallel, AffineMap, AffineMap.ext_linear, AffineEquiv.constVAdd, LinearMap.toAffineMap, AffineMap.toConstProdLinearMap, addGroupIsAddTorsor, AffineEquiv.vaddConst, NormedAddTorsor, Finset.weightedVSub, affineSpan, eq_affineCombination_of_mem_affineSpan, AffineIndependent, AffineBasis, AffineIndependent.vectorSpan_eq_top_of_card_eq_finrank_add_one, AffineBasis.coord, Affine.Triangle, Finset.centroid, AffineBasis.toMatrix_vecMul_coords, AffineSubspace.map, MvPolynomial.zeroLocus, MvPolynomial, MvPolynomial.vanishingIdeal_zeroLocus_eq_radical |
| Q1662573 | Akaike information criterion | InformationTheory.klDiv |
| Q908627 | Aleph number | Cardinal.aleph0, Cardinal.mk_eq_aleph0, Cardinal.aleph0_le_mk_iff, Cardinal.succ_aleph0, Cardinal.aleph_one_le_iff, Cardinal.continuum, Cardinal.aleph, Ordinal.cof, Cardinal.instSuccOrder, Ordinal.omega, Cardinal.mem_range_aleph_iff, Cardinal.isNormal_aleph, Ordinal.le_omega_self, Cardinal.aleph_lt_aleph, Cardinal.ord_aleph, Cardinal.range_aleph |
| Q3968 | Algebra | Algebra, Add, mul_comm, Eq, LT, Polynomial, Polynomial.degree, MvPolynomial, mul_eq_zero, quadratic_eq_zero_iff, Complex.exists_root, Matrix, Module, LinearMap, LinearMap.toMatrix, Mul, Nat.instAddCommMonoid, Group, mul_assoc, MulOneClass, Int.instAddCommGroup, Ring, CommRing, Field, Complex.instField, Polynomial.isNoetherianRing, IsGalois.intermediateFieldEquivSubgroup, Semigroup, MonoidHom, MulEquiv, CategoryTheory.Category, Metric.sphere |
| Q1000660 | Algebra over a field | Algebra, Matrix.instAlgebra, lie_jacobi, LinearMap.mul, AlgHom, AlgEquiv, Subalgebra, Algebra.TensorProduct.leftAlgebra, Unitization, DualNumber, MonoidAlgebra, Polynomial.algebraOfAlgebra, ContinuousMap.algebra, IncidenceAlgebra, Module.End.instAlgebra, NormedAlgebra, CStarAlgebra, LieAlgebra, RingHom.toAlgebra, Subring.center, Algebra.instSubtypeMemSubringCenter, Ring.toIntAlgebra |
| Q266237 | Algebraic curve | FunctionField, WeierstrassCurve.IsElliptic, WeierstrassCurve.exists_variableChange_isShortNF, WeierstrassCurve.Affine.Point.instAddCommGroup |
| Q180969 | Algebraic geometry | MvPolynomial, MvPolynomial.zeroLocus, MvPolynomial.vanishingIdeal, PrimeSpectrum.zariskiTopology, MvPolynomial.vanishingIdeal_zeroLocus_eq_radical, MvPolynomial.isNoetherianRing, IsIrreducible, TopologicalSpace.NoetherianSpace.exists_finset_irreducible, PrimeSpectrum.isIrreducible_iff_vanishingIdeal_isPrime, ContinuousMap.exists_restrict_eq, AlgebraicGeometry.Scheme.functionField, AlgebraicGeometry.Scheme.RationalMap, Projectivization, ProjectiveSpectrum.zeroLocus, AlgebraicGeometry.Scheme, AlgebraicGeometry.AffineScheme.equivCommRingCat |
| Q2553675 | Algebraic K-theory | Matrix.transvection |
| Q168817 | Algebraic number | IsAlgebraic, isAlgebraic_int, algebraicClosure, Transcendental, isAlgebraic_rat, GaussianInt, Real.isAlgebraic_cos_rat_mul_pi, IsFractionRing.isAlgebraic_iff, minpoly, Algebraic.countable, IntermediateField.adjoin.finiteDimensional, IntermediateField.finiteDimensional_adjoin, Subalgebra.algebraicClosure, algebraicClosure.isAlgClosure, IsIntegral, integralClosure, NumberField.RingOfIntegers |
| Q616608 | Algebraic number field | NumberField, Field, Module, FiniteDimensional, Rat.numberField, CyclotomicField, Algebra.IsAlgebraic, Algebra.IsAlgebraic.of_finite, IsAlgebraic, Polynomial.Monic, IsIntegral, isIntegral_algebraMap, GCDMonoid.toIsIntegrallyClosed, IsIntegral.add, NumberField.RingOfIntegers, IsDedekindDomain, Ideal.uniqueFactorizationMonoid, EuclideanDomain.to_principal_ideal_domain, NumberField.classNumber, ClassGroup, NumberField.RingOfIntegers.instFintypeClassGroup, NumberField.classNumber_eq_one_iff, NumberField.dedekindZeta, Ideal.absNorm, riemannZeta, NumberField.tendsto_sub_one_mul_dedekindZeta_nhdsGT, DirichletCharacter.LFunction, Nat.infinite_setOf_prime_and_eq_mod, NumberField.RingOfIntegers.basis, PowerBasis, Field.exists_primitive_element, Algebra.lmul, Algebra.trace, Algebra.traceForm, NumberField.discr, Matrix.aeval_self_charpoly, AbsoluteValue, UniformSpace.Completion, Rat.AbsoluteValue.equiv_real_or_padic, padicNorm, Padic, NumberField.InfinitePlace.isReal_or_isComplex, NumberField.IsTotallyReal, IsNonarchimedean, IsDedekindDomain.HeightOneSpectrum.intValuation_le_one, NumberField.FinitePlace.equivHeightOneSpectrum, IsDedekindDomain.HeightOneSpectrum.valuation, IsLocalization.AtPrime.isDiscreteValuationRing_of_dedekind_domain, Ideal.exists_ideal_over_prime_of_isIntegral, Ideal.LiesOver, hensels_lemma, Ideal.ramificationIdx, Ideal.inertia, NumberField.not_dvd_discr_iff_forall_liesOver, AlgEquiv, IsCyclotomicExtension.autEquivPow, Field.absoluteGaloisGroup, IsGalois.intermediateFieldEquivSubgroup, groupCohomology, BrauerGroup, FunctionField, NumberField.Units.rank_modTorsion, MeasureTheory.exists_ne_zero_mem_lattice_of_measure_mul_two_pow_lt_measure |
| Q613048 | Algebraic number theory | PythagoreanTriple, NumberField.Units.exist_unique_eq_mul_prod, Real.exists_int_int_abs_mul_sub_le, Ideal, Prime, Associated, UniqueFactorizationMonoid, Irreducible, Ideal.uniqueFactorizationMonoid, Nat.Prime.sq_add_sq, FractionalIdeal, ClassGroup, NumberField.classNumber, NumberField.InfinitePlace.IsReal, NumberField.InfinitePlace.card_add_two_mul_card_eq_rank, NumberField.mixedEmbedding, NumberField.mixedEmbedding.mixedSpace, NumberField.discr, padicNorm, Rat.AbsoluteValue.equiv_real_or_padic, NumberField.FinitePlace, NumberField.AdeleRing, Int.isUnit_iff, NumberField.Units.regulator, NumberField.dedekindZeta, IsDedekindDomain.HeightOneSpectrum.adicCompletion, NumberField.RingOfIntegers.instFintypeClassGroup, legendreSym.quadratic_reciprocity, NumberField.tendsto_sub_one_mul_dedekindZeta_nhdsGT |
| Q205464 | Algebraic structure | CommMagma, Semigroup, LeftDistribClass, RightDistribClass, Distrib, MulOneClass, IsUnit, Group, DivisionRing, CommGroup, Ring, CommRing, Field, CompleteLattice, BoundedOrder, DistribLattice, Set.instBooleanAlgebra, BooleanAlgebra, Module, Algebra, InnerProductSpace, IsTopologicalGroup, LieGroup, IsOrderedRing, Archimedean, NormedSpace, VonNeumannAlgebra, GrpCat |
| Q212803 | Algebraic topology | subgroupIsFreeOfIsFree, HomotopyGroup, FundamentalGroup, AlgebraicTopology.singularHomologyFunctor, HomologicalComplex.homology, IsManifold, Geometry.SimplicialComplex, Topology.CWComplex, AddCommGroup.equiv_free_prod_directSum_zmod, Complex.isAlgClosed |
| Q648995 | Algebraic variety | MvPolynomial.vanishingIdeal_zeroLocus_eq_radical, MvPolynomial.zeroLocus, MvPolynomial.vanishingIdeal, ProjectiveSpectrum.zeroLocus, WeierstrassCurve.IsElliptic, AlgebraicGeometry.Scheme |
| Q1047547 | Algebraically closed field | IsAlgClosed, Complex.isAlgClosed, AlgebraicClosure, IsAlgClosure, IsAlgClosure.equiv, IsAlgClosed.instInfinite, Polynomial.irreducible_of_degree_eq_one, IsAlgClosed.degree_eq_one_of_irreducible, Polynomial.IsRoot.dvd, Polynomial.exists_root_of_degree_eq_one, Polynomial.splits_iff_exists_multiset, Polynomial.Splits.exists_eval_eq_zero, Polynomial.uniqueFactorizationMonoid, Polynomial.finrank_quotient_span_eq_natDegree, minpoly.two_le_natDegree_iff, Algebra.IsAlgebraic.of_finite, Module.End.hasEigenvalue_iff_isRoot_charpoly, Module.End.exists_eigenvalue, Polynomial.roots_C_mul, Polynomial.aeval_ne_zero_of_isCoprime, Polynomial.isCoprime_iff_aeval_ne_zero_of_isAlgClosed, IsSepClosed.hasEnoughRootsOfUnity, IsCyclotomicExtension, FirstOrder.Field.ACF_isComplete, FirstOrder.Field.ACF_zero_realize_iff_finite_ACF_prime_not_realize |
| Q8366 | Algorithm | Nat.gcd, Nat.Partrec, Turing.TM0.Machine, List.mergeSort |
| Q339495 | Altitude (triangle) | Affine.Simplex.altitude, Affine.Simplex.altitudeFoot, Affine.Simplex.height, Affine.Triangle.orthocenter |
| Q333464 | Analysis of algorithms | Asymptotics.IsBigO |
| Q215084 | Analytic function | AnalyticOnNhd, HasFPowerSeriesAt, AnalyticAt, AnalyticAt.aeval_polynomial, NormedSpace.exp_analytic, Complex.analyticAt_sin, analyticAt_clog, expNegInvGlue.not_analyticAt_zero, AnalyticAt.add, AnalyticAt.inv, AnalyticAt.contDiffAt, AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq, AnalyticOnNhd.contDiffOn, DifferentiableOn.analyticOnNhd, Differentiable.apply_eq_apply_of_bounded, HasFPowerSeriesOnBall, FormalMultilinearSeries.radius, NormedSpace.expSeries_radius_eq_top, differentiableOn_riemannZeta |
| Q134787 | Analytic geometry | polarCoord, EuclideanSpace.sphere_zero_eq, AffineMap.lineMap, EuclideanSpace.dist_eq, dotProduct, EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two, InnerProductGeometry.cos_angle |
| Q10843274 | Analytic number theory | Nat.primeCounting, Chebyshev.pi_le_log4_mul_div, Nat.exists_prime_lt_and_le_two_mul, RiemannHypothesis, riemannZeta_ne_zero_of_one_le_re, Nat.exists_infinite_primes, Nat.infinite_setOf_prime_and_eq_mod, Nat.sum_four_squares, LSeries, LSeriesSummable_of_abscissaOfAbsConv_lt_re, LSeries_convolution, riemannZeta_eulerProduct_tprod, not_summable_one_div_on_primes, differentiableAt_riemannZeta |
| Q58413 | Ancient Greek mathematics | EuclideanGeometry.Sphere.thales_theorem, EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two, EuclideanGeometry.Sphere.IsTangentAt.mem_and_mem_iff_eq, irrational_sqrt_natCast_iff, Nat.gcd, Nat.exists_infinite_primes, Even.mul_right, Int.ModEq, DedekindCut |
| Q11352 | Angle | EuclideanGeometry.angle, Orientation.oangle, EuclideanGeometry.angle_add_of_ne_of_ne, Sbtw.oangle_eq_left_right, EuclideanGeometry.angle_add_angle_add_angle_eq_pi, Real.Angle.angle_eq_iff_two_pi_dvd_sub, InnerProductGeometry.cos_angle, InnerProductGeometry.angle |
| Q670036 | Arc length | Manifold.pathELength, Manifold.pathELength_comp_of_monotoneOn, eVariationOn.add_point, eVariationOn, BoundedVariationOn, variationOnFromTo, MeasureTheory.Measure.hausdorffMeasure, EuclideanSpace.dist_eq |
| Q11500 | Area | Real.volume_Icc_pi, MeasureTheory.measureReal_nonneg, MeasureTheory.measure_union_add_inter, MeasureTheory.measure_diff, EuclideanSpace.volume_ball_fin_two, volume_regionBetween_eq_integral |
| Q11205 | Arithmetic | Nat, Int, Cardinal, Ordinal, Rat, Irrational, Real, MulOneClass, mul_inv_cancel, CommMagma, Semigroup, Add, Finset.sum, sub_eq_add_neg, add_zero, add_comm, Mul, div_eq_mul_inv, mul_one, mul_comm, Monoid.npow, Real.rpow, Real.log, nsmul_eq_mul, npowBinRec, Nat.primeFactorsList_unique, Nat.exists_infinite_primes, FermatLastTheorem, add_div, div_mul_div_comm, Real.rpow_pos_of_pos, round, ZMod, Matrix, Nat.zero, Nat.succ, Nat.succ_injective, Nat.succ_ne_zero, Nat.rec |
| Q140744 | Arithmetic function | ArithmeticFunction, ArithmeticFunction.sigma, Nat.Coprime, ArithmeticFunction.IsMultiplicative, Nat.factorization_prod_pow_eq_self, padicValNat, ArithmeticFunction.cardDistinctFactors, ArithmeticFunction.sigma_one_apply, ArithmeticFunction.sigma_zero_apply, Nat.totient, ArithmeticFunction.moebius, ArithmeticFunction.moebius_apply_one, ArithmeticFunction.liouville, map_mul, jacobiSym, legendreSym, ArithmeticFunction.cardDistinctFactors_mul, ArithmeticFunction.cardFactors_mul, padicValNat.mul, Nat.primeCounting, Chebyshev.theta, Chebyshev.psi, ArithmeticFunction.vonMangoldt, ArithmeticFunction.carmichael, ArithmeticFunction.carmichael_pow_of_prime_ne_two, NumberField.classNumber, LSeries, ArithmeticFunction.LSeries_zeta_mul_Lseries_moebius, ArithmeticFunction.mul_apply, ArithmeticFunction.coe_zeta_mul_apply, ArithmeticFunction.sum_eq_iff_sum_mul_moebius_eq, ArithmeticFunction.IsMultiplicative.mul, Nat.sum_four_squares, Summable.tsum_mul_tsum_eq_tsum_sum_antidiagonal, jacobiSym.quadratic_reciprocity |
| Q19033 | Arithmetic mean | MeasureTheory.average, Finset.centerMass, Finset.centerMass_le_sup |
| Q669094 | Arithmetical hierarchy | ComputablePred.computable_iff_re_compl_re |
| Q177251 | Associative property | mul_assoc, Semigroup, BinaryTree.treesOfNumNodesEq_card_eq_catalan, Real.instField, gcd_assoc, Set.inter_assoc, Function.comp_assoc, CategoryTheory.Category.assoc, Matrix.mul_assoc, max_assoc |
| Q752718 | Asymptotic analysis | Asymptotics.IsEquivalent, Asymptotics.isEquivalent_iff_tendsto_one, Asymptotics.isEquivalent_zero_iff_eventually_zero, Asymptotics.IsEquivalent.refl, Asymptotics.IsEquivalent.rpow, Asymptotics.IsEquivalent.div, Stirling.factorial_isEquivalent_stirling |
| Q755991 | Atiyah–Singer index theorem | IsManifold, ContMDiffVectorBundle |
| Q1134435 | Automorphic form | eisensteinSeriesMF |
| Q202785 | Average | Finset.expect |
| Q17736 | Axiom | FirstOrder.Language.Theory, ConditionallyCompleteLinearOrderedField.uniqueOrderRingIso, FirstOrder.Language.exists_elementaryEmbedding_card_eq |
| Q179692 | Axiom of choice | Classical.axiomOfChoice, Classical.nonempty_pi, Classical.em, Cardinal.linearOrder, Cardinal.mul_eq_self, Function.Surjective.hasRightInverse, exists_wellOrder, IsChain.exists_maxChain, zorn_le, Order.IsOfFiniteCharacter.exists_maximal, Cardinal.sum_lt_prod, Module.Basis.ofVectorSpace, Ideal.exists_maximal, Module.Projective.of_free, Module.Baer.injective, CategoryTheory.Projective.Type.enoughProjectives, IsCompact.extremePoints_nonempty, isCompact_univ_pi, closure_pi_set, FirstOrder.Language.exists_elementarySubstructure_card_eq, CategoryTheory.skeleton_isSkeleton, CategoryTheory.isRightAdjoint_of_preservesLimits_of_solutionSetCondition, Ultrafilter.exists_le, Set.countable_iUnion, Set.Infinite.exists_subset_countable_infinite, AlgebraicClosure, exists_isTranscendenceBasis, subgroupIsFreeOfIsFree, Complex.nonempty_linearEquiv_real, continuous_iff_seqContinuous, isCompact_iff_isSeqCompact, exists_extension_norm_eq, exists_hilbertBasis, WeakDual.isCompact_polar, BaireSpace.of_completelyPseudoMetrizable, isCompact_iff_totallyBounded_isComplete, StoneCech, exists_continuous_zero_one_of_isClosed, ContinuousMap.exists_restrict_eq, PartitionOfUnity, FirstOrder.Language.Theory.isSatisfiable_iff_isFinitelySatisfiable, Cardinal.lt_wf, hahnEmbedding_isOrderedAddMonoid |
| Q1361825 | Axiom schema of replacement | ZFSet.image, ZFSet.mem_image, Ordinal.omega |
| Q838611 | Ball (mathematics) | Metric.closedBall, Metric.ball, EuclideanSpace.volume_ball, Nat.doubleFactorial, FiniteDimensional.of_isCompact_closedBall, convex_ball, Bornology.IsBounded, TotallyBounded, Metric.isOpen_iff, Metric.closure_ball_subset_closedBall, PiLp, gaugeSeminorm |
| Q220680 | Banach fixed-point theorem | ContractingWith, ContractingWith.exists_fixedPoint, ContractingWith.apriori_dist_iterate_fixedPoint_le, LipschitzWith, IsPicardLindelof.exists_eq_forall_mem_Icc_hasDerivWithinAt, HasStrictFDerivAt.toOpenPartialHomeomorph, ContractingWith.isFixedPt_fixedPoint_iterate, Function.IsFixedPt, CompleteSpace |
| Q194397 | Banach space | CompleteSpace, NormedSpace, dist_eq_norm, CauchySeq, NormedAddCommGroup.summable_imp_tendsto_iff_completeSpace, NormedAddCommGroup, BaireSpace, Metric.closedBall, FiniteDimensional.of_isCompact_closedBall, FiniteDimensional.complete, HilbertBasis.repr, BaireSpace.instBarrelledSpace, UniformSpace.Completion, SemilinearMapClass.bound_of_continuous, ContinuousLinearMap.completeSpace, ContinuousLinearMap.toNormedRing, ContinuousLinearEquiv, LinearIsometryEquiv, CompleteSpace.prod, quotient_norm_mk_eq, Submodule.Quotient.completeSpace, Submodule.ClosedComplemented, lp, InnerProductSpace, MeasureTheory.L2.innerProductSpace, NormedAlgebra, ContinuousMap.instNormedCommRing, CStarAlgebra, StrongDual, exists_extension_norm_eq, exists_dual_vector, geometric_hahn_banach_closed_point, exists_extension_of_le_sublinear, WeakSpace, Convex.toWeakSpace_closure, Module.Dual, WeakDual, WeakDual.isCompact_closedBall, InnerProductSpace.toDual, gelfandTransform_bijective, NormedSpace.inclusionInDoubleDual, NormedSpace.inclusionInDoubleDualLi, banach_steinhaus, ContinuousLinearMap.isOpenMap, ContinuousLinearEquiv.ofBijective, ContinuousLinearMap.ofIsClosedGraph, WeakDual.metrizable_of_isCompact, GeneralSchauderBasis, GeneralSchauderBasis.coord, TensorProduct, TensorProduct.lift, TensorProduct.tmul, InnerProductSpace.ofNorm, inner_eq_sum_norm_sq_div_four, parallelogram_law_with_norm, IsometryEquiv.toRealAffineIsometryEquiv, fderiv, convexHull, ContinuousLinearMap.opNorm, IsBoundedLinearMap |
| Q737851 | Banach–Tarski paradox | Equidecomp, FreeGroup, Equidecomp.trans |
| Q189569 | Basis (linear algebra) | Module.Basis, Module.Basis.mk, mk_eq_mk_of_basis, LinearIndependent, Submodule.span, linearIndependent_iff_notMem_span, Module.Basis.linearCombination_repr, FiniteDimensional, Pi.basisFun, Polynomial.Sequence.basis, Module.Basis.extend, Module.Basis.ofVectorSpace, Module.Basis.maximal, basisOfLinearIndependentOfCardEqFinrank, basisOfTopLeSpanOfCardEqFinrank, Module.Basis.coord, Module.Basis.equivFun, Module.Basis.toMatrix, Module.Basis.toMatrix_mul_toMatrix, Module, Module.Free, Finsupp.basisSingleOne, fourierBasis, AffineBasis |
| Q182505 | Bayes' theorem | ProbabilityTheory.cond_eq_inv_mul_cond_mul, ProbabilityTheory.cond, ProbabilityTheory.cond_mul_eq_inter, ProbabilityTheory.posterior_eq_withDensity, MeasureTheory.Measure.withDensity_rnDeriv_eq |
| Q812535 | Bayesian inference | ProbabilityTheory.cond_eq_inv_mul_cond_mul, ProbabilityTheory.cond, ProbabilityTheory.posterior_eq_withDensity, ProbabilityTheory.cond_mul_eq_inter, ProbabilityTheory.posterior, MeasureTheory.Measure.absolutelyContinuous_iff_withDensity_rnDeriv_eq |
| Q812534 | Bayesian probability | ProbabilityTheory.posterior |
| Q388525 | Bell's theorem | CHSH_inequality_of_comm, tsirelson_inequality, HilbertBasis, IsCHSHTuple |
| Q518831 | Bernoulli process | PMF.bernoulli, MeasureTheory.cylinder, ProbabilityTheory.bernoulliMeasure, ProbabilityTheory.strong_law_ae, Nat.choose, ProbabilityTheory.binomial, ProbabilityTheory.binomial_one_eq_bernoulliMeasure, ProbabilityTheory.tendstoInDistribution_inv_sqrt_mul_sum, ProbabilityTheory.measure_zero_or_one_of_measurableSet_limsup_atTop, Cardinal.cantorFunction, cantorSet |
| Q269878 | Big O notation | Asymptotics.IsBigO, Asymptotics.isBigO_iff_div_isBoundedUnder, Polynomial.isEquivalent_atTop_lead, Filter.IsBoundedUnder.isBigO_one, Asymptotics.IsBigO.add, Asymptotics.IsBigO.const_mul_left, Asymptotics.IsBigO.trans, Asymptotics.isLittleO_pow_pow_atTop_of_lt, isLittleO_log_rpow_atTop, isLittleO_rpow_exp_atTop, isLittleO_pow_pow_of_lt_left, Asymptotics.IsTheta, Asymptotics.IsTheta.isBigO, Asymptotics.IsLittleO, Asymptotics.IsLittleO.isBigO, Asymptotics.IsLittleO.add, Asymptotics.IsLittleO.trans, Asymptotics.IsEquivalent, Asymptotics.IsEquivalent.trans, Stirling.factorial_isEquivalent_stirling, isBigO_riemannZeta_sub_one_div |
| Q180907 | Bijection | Function.Bijective, Function.bijective_iff_has_inverse, Fintype.equivFin, Equiv.Perm, Function.Surjective, Function.bijective_id, Function.Embedding.schroeder_bernstein, Equiv.symm, Function.Bijective.comp, Fintype.card_eq, Denumerable, Equiv.Perm.permGroup, Cardinal.mk_congr, Finite.injective_iff_bijective, CategoryTheory.isIso_iff_bijective, PEquiv |
| Q4907197 | Bijection, injection and surjection | Function.Injective, Function.Surjective, Function.Bijective, Function.injective_iff_hasLeftInverse, Equiv.ofInjective, Function.Injective.comp, Function.Embedding.injective, Function.surjective_iff_hasRightInverse, Setoid.quotientKerEquivOfSurjective, Function.Surjective.comp, Function.bijective_iff_has_inverse, Function.Bijective.comp, Equiv.Perm.permGroup, Cardinal.eq, Cardinal.le_def, Function.bijective_id, Real.expOrderIso, Set.image_preimage_subset, CategoryTheory.mono_iff_injective |
| Q3913 | Binary number | Nat.ofDigits_digits, Nat.ofDigits_eq_sum_mapIdx, Nat.bitwise, Nat.shiftLeft_eq_mul_pow, Nat.digits_def' |
| Q380172 | Binary tree | Tree, Tree.numLeaves_eq_numNodes_succ, Tree.treesOfNumNodesEq_card_eq_catalan, BinaryTree.treesOfNumNodesEq_succ, DyckWord.card_dyckWord_semilength_eq_catalan, DyckWord.equivTree |
| Q185547 | Binomial distribution | ProbabilityTheory.binomial, PMF.bernoulli, PMF.binomial_one_eq_bernoulli, PMF.binomial_apply, ProbabilityTheory.tendsto_choose_mul_pow_of_tendsto_mul_atTop |
| Q833480 | Binomial series | binomialSeries, Ring.choose, Complex.one_add_cpow_hasFPowerSeriesOnBall_zero, binomialSeries_radius_eq_one, Complex.GammaSeq_tendsto_Gamma, Complex.one_div_one_sub_cpow_hasFPowerSeriesOnBall_zero, Ring.multichoose, Complex.one_div_one_sub_hasFPowerSeriesOnBall_zero, Complex.one_div_one_sub_sq_hasFPowerSeriesOnBall_zero, Complex.one_div_one_sub_pow_hasFPowerSeriesOnBall_zero |
| Q751484 | Block design | Matrix.IsHadamard |
| Q4973304 | Boolean algebra (structure) | DistribLattice.booleanAlgebraOfComplemented, BooleanAlgebra.toBooleanRing, BooleanAlgebra, PUnit.instBooleanAlgebra, inf_eq_left, BooleanAlgebra.toBoundedOrder, inf_eq_iInf, compl_unique, OrderDual.instBooleanAlgebra, Bool.instBooleanAlgebra, Set.instBooleanAlgebra, TopologicalSpace.Clopens.instBooleanAlgebra, instBooleanAlgebraSubtypeIsIdempotentElem, BoundedLatticeHom, map_compl', OrderIso, symmDiff_eq, BooleanRing.toBooleanAlgebra, boolRingCatEquivBoolAlg, Order.Ideal, Order.Ideal.IsPrime, Order.Ideal.IsMaximal, Order.Ideal.IsPrime.isMaximal, Order.PFilter, Ultrafilter.exists_le, GeneralizedBooleanAlgebra |
| Q1144897 | Brouwer fixed-point theorem | exists_mem_Icc_isFixedPt_of_mapsTo |
| Q214728 | Bézier curve | bernsteinPolynomial, Finset.affineCombination, AffineMap.lineMap, AffineMap.lineMap_apply_module, Nat.choose |
| Q263809 | C*-algebra | CStarAlgebra, ZeroAtInftyContinuousMap.instNonUnitalCommCStarAlgebra, CStarRing.norm_star_mul_self, StarAlgHom, NonUnitalStarAlgHom.norm_apply_le, StarAlgEquiv, StarSubalgebra.cstarAlgebra, IsSelfAdjoint, nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts, CStarAlgebra.increasingApproximateUnit, Matrix.instCStarRing, instCStarAlgebraContinuousLinearMapComplexIdOfCompleteSpace, gelfandStarTransform, VonNeumannAlgebra |
| Q729471 | Cantor's diagonal argument | Uncountable, Function.cantor_surjective, Cardinal.not_countable_real, Cardinal.cantorFunction_injective, Cardinal.cantor, Cardinal.le_def, Function.Embedding.schroeder_bernstein, ComputablePred.halting_problem |
| Q474881 | Cantor's theorem | Cardinal.cantor, Cardinal.mk_real, Cardinal.le_def, Function.cantor_surjective, Cardinal.aleph0_lt_continuum, Function.exists_fixed_point_of_surjective |
| Q163875 | Cardinal number | Cardinal, Cardinal.eq, Rat.instDenumerable, Cardinal.cantor, Cardinal.aleph_zero, Cardinal.isEquivalent, Cardinal.mk, Cardinal.add_one_eq, Cardinal.mk_real, Ordinal.IsInitial, Ordinal.isInitial_natCast, Cardinal.aleph, Ordinal.omega, Cardinal.isSuccLimit_omega, Cardinal.le_def, Function.Embedding.schroeder_bernstein, Cardinal.lt_aleph0, Cardinal.mem_range_aleph_iff, Cardinal.power_natCast, Order.succ, Cardinal.add_def, Cardinal.commSemiring, Cardinal.addLeftMono, Cardinal.add_eq_max, Cardinal.canonicallyOrderedAdd, Cardinal.mul_def, Cardinal.noZeroDivisors, Cardinal.isOrderedRing, Cardinal.mul_eq_max, Cardinal.dvd_of_le_of_aleph0_le, Cardinal.power_def, Cardinal.power_zero, Cardinal.zero_power, Cardinal.one_power, Cardinal.power_one, Cardinal.power_add, Cardinal.power_mul, Cardinal.mul_power, Cardinal.power_le_power_right, Cardinal.instNoMaxOrder, Cardinal.nat_power_eq, Cardinal.power_nat_eq, Cardinal.lt_power_cof_ord, Fintype.card_eq, Denumerable, Set.countable_infinite_iff_nonempty_denumerable, Denumerable.prod, Algebraic.countable, Cardinal.aleph0 |
| Q4049983 | Cardinality | Cardinal.mk, Cardinal.eq, Set, Cardinal.aleph0, Function.Injective, Function.Surjective, Function.Bijective, Equiv.refl, Equiv.symm, Equiv.trans, Cardinal.le_def, Function.Embedding.schroeder_bernstein, Ordinal.type, WellOrderingRel, Countable, Set.Countable, Rat, Cardinal.mkRat, IsAlgebraic, Transcendental, Algebraic.countable, Uncountable, Cardinal.not_countable_real, Cardinal.mk_set_nat, Cardinal.mk_real, Cardinal.cantor, Cardinal, Nat.card, Finite.injective_iff_surjective, Cardinal.add_def, Cardinal.mk_prod, Finset.inclusion_exclusion_card_biUnion, Finite, Cardinal.aleph, Ordinal, Ordinal.omega0, Ordinal.omega, Cardinal.aleph_succ, Cardinal.mem_range_aleph_iff, Cardinal.mul_def, Cardinal.sum_lt_prod, Cardinal.add_eq_self, Cardinal.mk_arrow, Cardinal.power_zero, Cardinal.mk_set, not_small_cardinal, not_small_ordinal, Real, Cardinal.continuum, Cardinal.mk_Ioo_real, Real.tanOrderIso, cantorSet, Cardinal.continuum_power_aleph0, Cardinal.aleph0_lt_continuum, Cardinal.beth, ZFSet.omega, ZFSet.powerset, ZFSet.choice, Cardinal.IsInaccessible, ZFSet.vonNeumann, Finset.card_lt_card, Pi.uniqueOfIsEmpty, Cardinal.mk_nat, ZFSet, Prod, Sum, Cardinal.IsRegular |
| Q22952648 | Cardinality of the continuum | Cardinal.continuum, Cardinal.mk_set_nat, Cardinal.eq, Cardinal.mk_Ioo_real, Cardinal.aleph0, Cardinal.aleph, Cardinal.not_countable_real, Cardinal.cantor, Function.Embedding.schroeder_bernstein, Cardinal.mk_real, Cardinal.continuum_power_aleph0, Cardinal.mk_powerset, Cardinal.beth, Cardinal.beth_one, Cardinal.sum_lt_prod, Algebraic.cardinalMk_of_countable_of_charZero, Cardinal.aleph0_lt_continuum, Cardinal.mk_complex |
| Q62912 | Cartesian coordinate system | OrthonormalBasis, EuclideanSpace, Metric.sphere, EuclideanSpace.equiv, EuclideanSpace.dist_eq, EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two, IsometryEquiv, AffineEquiv.constVAdd, Orientation.rotation, LinearMap.toMatrix_comp, AffineMap, AffineIsometryEquiv, Matrix.transvection, Orientation, Module.Oriented.positiveOrientation, EuclideanSpace.basisFun, Complex.equivRealProd |
| Q719395 | Category (mathematics) | CategoryTheory.Category, RingCat, TopCat, CategoryTheory.Equivalence, CategoryTheory.Functor, CategoryTheory.SingleObj, Quiver.Hom, CategoryTheory.SmallCategory, CategoryTheory.LocallySmall, CategoryTheory.types, CategoryTheory.RelCat, CategoryTheory.Discrete, Preorder.smallCategory, Quiver.IsThin, CategoryTheory.Iso, CategoryTheory.Groupoid, FundamentalGroup, FundamentalGroupoid, Quiver, CategoryTheory.Paths, Preord, CategoryTheory.ConcreteCategory, GrpCat, Ab, CategoryTheory.ObjectProperty.FullSubcategory, CategoryTheory.Cat, CategoryTheory.Functor.category, CategoryTheory.NatTrans, CategoryTheory.Category.opposite, CategoryTheory.prod, CategoryTheory.Quotient, CategoryTheory.Over, CategoryTheory.Under, CategoryTheory.Comma, CategoryTheory.MorphismProperty.Localization, CategoryTheory.Mono, CategoryTheory.Epi, CategoryTheory.IsSplitEpi, CategoryTheory.IsSplitMono, CategoryTheory.IsIso, CategoryTheory.End, CategoryTheory.End.monoid, CategoryTheory.Aut, CategoryTheory.IsSplitEpi.epi, CategoryTheory.Preadditive, CategoryTheory.Limits.kernel, CategoryTheory.Limits.cokernel, CategoryTheory.Abelian, AddCommGrpCat, CategoryTheory.EnrichedCategory, CategoryTheory.Limits.HasLimits, CategoryTheory.Limits.Types.hasLimitsOfSize, CategoryTheory.MonoidalClosed |
| Q217413 | Category theory | CategoryTheory.Category, CategoryTheory.types, CategoryTheory.Mono, CategoryTheory.SplitEpi.epi, CategoryTheory.Functor, CategoryTheory.Functor.op, CategoryTheory.NatTrans, CategoryTheory.NatTrans.isIso_iff_isIso_app, CategoryTheory.Functor.category, CategoryTheory.Bicategory.Strict |
| Q217847 | Cauchy sequence | CauchySeq, IsCauSeq, Metric.cauchySeq_iff, CompleteSpace, UniformSpace.Completion, Real.instCompleteSpace, Filter.Tendsto.cauchySeq, CauchySeq.isBounded_range, tendsto_nhds_of_cauchySeq_of_subseq, UniformContinuous.comp_cauchySeq, CauchySeq.mul |
| Q913764 | Cauchy's integral formula | DiffContOnCl.circleIntegral_sub_inv_smul, DifferentiableOn.analyticOnNhd, DiffContOnCl.circleIntegral_one_div_sub_center_pow_smul, DifferentiableOn.contDiffOn, TendstoLocallyUniformlyOn.differentiableOn, Complex.IsConservativeOn.isExactOn_ball, Complex.norm_iteratedDeriv_le_of_forall_mem_sphere_norm_le, Differentiable.exists_const_forall_eq_of_bounded, DiffContOnCl.circleAverage |
| Q190546 | Cauchy–Schwarz inequality | norm_inner_le_norm, norm_eq_sqrt_re_inner, norm_inner_eq_norm_iff, Finset.sq_sum_div_le_sum_sq_div, Finset.sum_mul_sq_le_sq_mul_sq, inner_mul_inner_self_le, norm_add_le, continuous_inner, InnerProductGeometry.angle, Real.inner_le_Lp_mul_Lq, PositiveLinearMap.norm_map_star_mul_le, discrim_le_zero, SimpleGraph.sum_degrees_eq_twice_card_edges, InnerProductSpace, LinearIndependent, ProbabilityTheory.variance, ProbabilityTheory.covariance, ContinuousLinearMap.opNorm, EuclideanSpace.inner_eq_star_dotProduct, PositiveLinearMap, CStarAlgebra, CompleteSpace, MeasureTheory.Lp, starRingEnd, PositiveLinearMap.preGNSpreInnerProdSpace |
| Q656772 | Cayley–Hamilton theorem | Matrix.aeval_self_charpoly, Matrix.charpoly, Matrix.pow_eq_aeval_mod_charpoly, Matrix.minpoly_dvd_charpoly, Matrix.charpoly_fin_two, Matrix.adjugate, Polynomial.div_modByMonic_unique, Submodule.eq_bot_of_le_smul_of_le_jacobson_bot |
| Q189156 | Cellular automaton | DihedralGroup |
| Q190391 | Central limit theorem | ProbabilityTheory.tendstoInDistribution_inv_sqrt_mul_sum_sub, ProbabilityTheory.strong_law_ae_real, ProbabilityTheory.tendsto_charFun_inv_sqrt_mul_pow, MeasureTheory.ProbabilityMeasure.tendsto_iff_tendsto_charFun, ProbabilityTheory.charFun_inv_sqrt_mul_sum, MeasureTheory.ProbabilityMeasure.tendsto_iff_forall_integral_tendsto, ProbabilityTheory.multivariateGaussian, MeasureTheory.charFun, ProbabilityTheory.gaussianReal, ProbabilityTheory.IdentDistrib, MeasureTheory.ae, MeasureTheory.convolution, MeasureTheory.SignedMeasure.totalVariation, MeasureTheory.TendstoInMeasure, MeasureTheory.Martingale, Finset.sum |
| Q511093 | Centroid | Affine.Simplex.eq_centroid_of_forall_mem_median, Finset.centroid, Affine.Triangle.dist_point_centroid, Affine.Simplex.dist_point_centroid, Affine.Simplex.centroid |
| Q207455 | Chain rule | HasDerivAt.comp, deriv_comp, HasDerivAt.div, HasDerivAt.of_local_left_inverse, Real.hasDerivAt_log, HasFTaylorSeriesUpToOn.comp, HasFDerivAt, HasFDerivAt.comp, HasDerivAt.add, HasDerivAt.mul, Real.hasDerivAt_exp, fderiv_comp, HasMFDerivAt.comp |
| Q166314 | Chaos theory | MulAction.IsTopologicallyTransitive, cantorSet |
| Q600043 | Character theory | FDRep.character, FDRep.char_one, FDRep.char_conj, FDRep.char_iso |
| Q5073783 | Characterizations of the exponential function | NormedSpace.exp_eq_tsum_div, NormedSpace.expSeries_radius_eq_top, Real.exp_add, NormedSpace.exp, Real.log_pow |
| Q619511 | Chebyshev polynomials | Polynomial.Chebyshev.T_real_cos, Polynomial.Chebyshev.U_real_cos, Polynomial.Chebyshev.leadingCoeff_eq_iff_of_forall_abs_le_one, Polynomial.Chebyshev.T_add_two, Polynomial.Chebyshev.U_add_two, Polynomial.Chebyshev.natDegree_T, Polynomial.Chebyshev.T_real_cosh, Polynomial.Chebyshev.T_eq_U_sub_X_mul_U, Polynomial.Chebyshev.T_derivative_eq_U, Polynomial.Chebyshev.T_eval_neg, Polynomial.Chebyshev.rootMultiplicity_T_real, Polynomial.Chebyshev.roots_T_real, Polynomial.Chebyshev.isExtrOn_T_real_iff, Polynomial.Chebyshev.derivative_T_eval_one, Polynomial.Chebyshev.iterate_derivative_T_eval_one, Polynomial.Chebyshev.T_mul_T, Polynomial.Chebyshev.T_mul, Polynomial.Chebyshev.integral_eval_T_real_mul_eval_T_real_measureT_of_ne, Polynomial.Chebyshev.one_sub_X_sq_mul_derivative_derivative_T_eq_poly_in_T, Polynomial.Chebyshev.leadingCoeff_le_of_forall_abs_le_one, Polynomial.dickson_one_one_eq_chebyshev_C, Polynomial.Chebyshev.T_two, Polynomial.Chebyshev.U_two, Polynomial.Chebyshev.C |
| Q249514 | Chebyshev's inequality | ProbabilityTheory.meas_ge_le_variance_div_sq, MeasureTheory.meas_ge_le_lintegral_div, MeasureTheory.mul_meas_ge_le_integral_of_nonneg, MeasureTheory.mul_meas_ge_le_pow_eLpNorm', ProbabilityTheory.measure_ge_le_exp_mul_mgf, ProbabilityTheory.measure_ge_le_exp_cgf |
| Q193878 | Chinese remainder theorem | Nat.chineseRemainderOfFinset, ZMod.chineseRemainder, Nat.chineseRemainder_modEq_unique, Ideal.quotientInfToPiQuotient_surj, Nat.chineseRemainder, Nat.chineseRemainderOfList, Ideal.quotientInfRingEquivPiQuotient, Lagrange.interpolate, Nat.chineseRemainder', Ideal.isCoprime_iff_exists, Ideal.prod_eq_iInf_of_pairwise_isCoprime, CompleteOrthogonalIdempotents, linearIndependent_monoidHom |
| Q309157 | Church–Turing thesis | Nat.Partrec, Turing.TM0.Machine, Turing.TM2Computable |
| Q17278 | Circle | Metric.sphere, EuclideanGeometry.Sphere.radius, EuclideanGeometry.Sphere.IsDiameter, Metric.closedBall, EuclideanGeometry.Sphere.center, EuclideanGeometry.Sphere.IsTangentAt, Theorems100.area_disc, circleMap, EuclideanGeometry.Sphere.IsTangentAt_iff_angle_eq_pi_div_two, Circle, AffineIndependent.existsUnique_dist_eq, EuclideanGeometry.Sphere.inner_vsub_center_midpoint_vsub, EuclideanGeometry.Sphere.oangle_center_eq_two_zsmul_oangle, EuclideanGeometry.Sphere.two_zsmul_oangle_eq, EuclideanGeometry.Sphere.angle_eq_pi_div_two_iff_mem_sphere_of_isDiameter, EuclideanGeometry.mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_pi, EuclideanGeometry.Sphere.IsTangentAt_of_angle_eq_pi_div_two, EuclideanGeometry.Sphere.IsTangentAt.angle_eq_pi_div_two, EuclideanGeometry.Sphere.IsTangentAt.dist_eq_of_mem_of_mem, EuclideanGeometry.mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_zero, EuclideanGeometry.Sphere.dist_sq_eq_mul_dist_of_tangent_and_secant, Affine.Simplex.insphere, Affine.Simplex.circumsphere |
| Q715746 | Circular motion | circleMap |
| Q17006917 | Classical orthogonal polynomials | Polynomial.Chebyshev.one_sub_X_sq_mul_derivative_derivative_T_eq_poly_in_T, Polynomial.Chebyshev.T_add_two, Polynomial.Chebyshev.abs_eval_T_real_le_one, Polynomial.Chebyshev.U, Polynomial.hermite |
| Q1340623 | Classification of finite simple groups | CompositionSeries.jordan_holder, Subgroup.exists_right_complement'_of_coprime |
| Q674689 | Clifford algebra | CliffordAlgebra, CliffordAlgebra.Rel, CliffordAlgebra.ι, CliffordAlgebra.ι_mul_ι_add_swap, ExteriorAlgebra, CliffordAlgebra.equivExterior, CliffordAlgebra.lift, CliffordAlgebra.forall_mul_self_eq_iff, CliffordAlgebra.hom_ext, CliffordAlgebra.map, LinearMap.BilinForm.exists_orthogonal_basis, CliffordAlgebra.ι_mul_ι_comm_of_isOrtho, QuadraticForm.equivalent_one_neg_one_weighted_sum_squared, sigPos, CliffordAlgebraRing.equiv, CliffordAlgebraComplex.equiv, CliffordAlgebraQuaternion.equiv, QuadraticForm.equivalent_weightedSumSquares_of_isAlgClosed, CliffordAlgebraDualNumber.equiv, CliffordAlgebra.gradedAlgebra, CliffordAlgebra.involute, CliffordAlgebra.evenOdd_isCompl, CliffordAlgebra.even, CliffordAlgebra.equivEven, CliffordAlgebra.reverse, CliffordAlgebra.instStarRing, Algebra.IsCentral, CliffordAlgebra.prodEquiv, lipschitzGroup, pinGroup |
| Q104845546 | Closed graph theorem (functional analysis) | LinearMap.continuous_of_isClosed_graph, IsBoundedLinearMap.isLinearMap_and_continuous_iff_isBoundedLinearMap, LinearPMap.IsClosed, LinearPMap.graph, IsClosed.mono, ContinuousLinearMap.isOpenMap |
| Q1283623 | Cofinality | Order.cof, Order.cof_eq_one_iff, Ordinal.cof_succ, IsCofinal.mem_of_isMax, Order.cof_nat, Ordinal.cof, Ordinal.cof_type, Ordinal.exists_isFundamentalSeq, Ordinal.cof_eq_aleph0_of_isSuccLimit, Ordinal.cof_zero, Cardinal.isRegular_cof, Cardinal.isRegular_aleph_add_one, Ordinal.cof_ord_cof, Cardinal.lt_power_cof_ord, Cardinal.isSingular_aleph_omega0, Ordinal.cof_omega |
| Q1198376 | Cohomology | CochainComplex, CochainComplex.HomComplex.Cocycle, TopCat.Homotopy.congr_homologyMap_singularChainComplexFunctor, CategoryTheory.Sheaf.H, AlgebraicGeometry.Scheme.EllAdicCohomology |
| Q825367 | Coin flipping | PMF.bernoulli |
| Q202805 | Combination | Finset.powersetCard, Finset.ext_iff, Finset.card_powersetCard, Nat.choose_eq_factorial_div_factorial, Sym, add_pow, Nat.choose_succ_succ, Nat.choose_eq_descFactorial_div_factorial, Nat.choose_symm, Nat.choose_mul_factorial_mul_factorial, Nat.add_one_mul_choose_eq, Nat.multichoose, Nat.multichoose_eq, Sym.card_sym_eq_choose, Finset.card_powerset, Nat.binomial_eq_choose |
| Q5150824 | Combinatorial design | Configuration.ProjectivePlane, Configuration.HasLines.card_le |
| Q76592 | Combinatorics | Nat.choose, Nat.choose_symm, Nat.choose_eq_factorial_div_factorial, Nat.choose_succ_succ, Nat.fib, YoungDiagram, Equiv.Perm, Lattice, BooleanAlgebra, IsAntichain.sperner, Finset.exists_ne_map_eq_of_card_lt_of_maps_to, Convex |
| Q966582 | Common logarithm | Real.logb, Real.logb_neg, Real.log_div_log |
| Q727659 | Commutative algebra | IsNoetherianRing, Polynomial.isNoetherianRing, Ideal.IsPrimary, Submodule.isLasker, Submodule.IsMinimalPrimaryDecomposition.image_radical_eq_associated_primes, IsLocalization, Rat.isFractionRing, AdicCompletion, PrimeSpectrum.zariskiTopology |
| Q621542 | Commutative diagram | QuotientGroup.quotientKerEquivRange, LinearMap.bijective_of_surjective_of_bijective_of_bijective_of_injective, CategoryTheory.Cat.bicategory, CategoryTheory.Bicategory, CategoryTheory.Functor |
| Q165474 | Commutative property | CommMagma, Commute, mul_comm, AddCommGroup, Set.union_comm, and_comm, cross_anticomm, CommSemigroup, CommMonoid, CommGroup, CommRing |
| Q858656 | Commutative ring | Ring, CommRing, Int.instCommRing, Field, Polynomial, ContinuousMap.instCommRingOfIsTopologicalRing, IsUnit, IsDomain, IsNilpotent, IsLocalization, IsFractionRing, Ideal.instIsTwoSided, Module, Module.Free, Module.Finite, Ideal, Ring.isField_iff_isSimpleOrder_ideal, Ideal.span, Submodule.IsPrincipal, IsPrincipalIdealRing, PrincipalIdealRing.to_uniqueFactorizationMonoid, Irreducible, Nat.primeFactorsList_unique, Prime, Prime.irreducible, Ideal.Quotient.commRing, ZMod, Ideal.IsMaximal, Ideal.Quotient.maximal_ideal_iff_isField_quotient, Ideal.exists_maximal, IsNoetherianRing, Polynomial.isNoetherianRing, IsArtinianRing, IsSemiprimaryRing.isNoetherian_iff_isArtinian, isArtinianRing_iff_isNoetherianRing_krullDimLE_zero, Ideal.IsPrime, Ideal.uniqueFactorizationMonoid, Ideal.IsMaximal.isPrime, Ideal.Quotient.isDomain_iff_prime, IsLocalRing, PrimeSpectrum, minimalPrimes.equivIrreducibleComponents, TopologicalSpace.NoetherianSpace.finite_irreducibleComponents, Submodule.isLasker, AlgebraicGeometry.AffineScheme, AlgebraicGeometry.Scheme.ΓSpecIso, ringKrullDim, ringKrullDim_eq_zero_of_field, instFiniteRingKrullDimOfIsLocalRing, RingHom, RingHom.ker, RingEquiv, Ideal.quotientInfRingEquivPiQuotient, CommRingCat.zIsInitial, add_pow, Algebra.TensorProduct.instCommRing, Algebra.FiniteType, IsLocalization.AtPrime.isLocalRing, IsLocalRing.ResidueField, Submodule.eq_smul_of_le_smul_of_le_jacobson, IsLocalRing.CotangentSpace, ringKrullDim_le_spanFinrank_maximalIdeal, IsRegularLocalRing, IsDiscreteValuationRing, Ideal.height_le_spanRank_toENat_of_mem_minimalPrimes, IsIntegrallyClosed, Ideal.adicTopology, AdicCompletion, IsAdicComplete, IsAdicComplete.henselianRing, Module.Projective, Module.free_of_flat_of_isLocalRing, Ext, Module.Flat, littleWedderburn, BooleanRing |
| Q1887083 | Compact group | IsTopologicalGroup, Subgroup.connectedComponentOfOne, ProfiniteGrp, PontryaginDual, MeasureTheory.Measure.haarMeasure |
| Q1780743 | Compact operator | IsCompactOperator, isCompactOperator_iff_isCompact_closure_image_closedBall, IsCompactOperator.continuous, IsCompactOperator.isCompact_closure_image_of_bounded, isCompactOperator_id_iff_finiteDimensional, isClosed_setOf_isCompactOperator, IsCompactOperator.clm_comp, IsCompactOperator.hasEigenvalue_or_mem_resolventSet, IsCompactOperator.hasEigenvalue_iff_mem_spectrum, ContinuousLinearMap.orthogonalComplement_iSup_eigenspaces_eq_bot |
| Q381892 | Compact space | IsCompact.exists_isMaxOn, CompactSpace, Metric.isCompact_iff_isClosed_bounded, IsCompact, tendsto_subseq_of_bounded, BoundedContinuousFunction.arzela_ascoli, CompactSpace.uniformContinuous_of_continuous, CompactIccSpace.isCompact_Icc, ProperSpace.isCompact_closedBall, isCompact_iff_compactSpace, lebesgue_number_lemma_of_metric, IsCompact.isBounded, CompleteLattice, ContinuousMap.evalAlgHom, IsClosed.isCompact, IsCompact.union, IsCompact.image, isCompact_univ_pi, isCompact_iff_isSeqCompact, Finite.compactSpace, IsCompact.isClosed, IsCompact.isComplete, SeparatedNhds.of_isCompact_isCompact, Continuous.homeoOfEquivCompactToT2, NormalSpace.of_compactSpace_r1Space, IsProperMap.isCompact_preimage, OnePoint, IsCompact.exists_isLUB, RealNormedSpace.noncompactSpace, compactSpace_of_completeLinearOrder, isCompact_sphere, WeakDual.isCompact_closedBall, isCompact_cantorSet, spectrum.isCompact, isCompact_closure_of_isTightMeasureSet, MeasureTheory.IsTightMeasureSet, PrimeSpectrum.compactSpace, WeakDual.CharacterSpace.instCompactSpaceElemCharacterSpaceOfProperSpace, ProfiniteGrp |
| Q45715 | Complete graph | SimpleGraph.completeGraph, Digraph.completeDigraph, SimpleGraph.card_edgeFinset_top_eq_card_choose_two, compl_top |
| Q848569 | Complete metric space | CompleteSpace, CauchySeq, IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed, IsClosed.isComplete, Real.instCompleteSpace, Pi.complete, BoundedContinuousFunction.instCompleteSpace, Padic.instCompleteSpace, IsCompact.isComplete, isCompact_iff_totallyBounded_isComplete, ProperSpace.isCompact_closedBall, IsComplete.isClosed, BaireSpace.of_completelyPseudoMetrizable, BaireSpace, ContractingWith.fixedPoint, HasStrictFDerivAt.toOpenPartialHomeomorph, UniformSpace.Completion, UniformSpace.Completion.extension_unique, AbstractCompletion.compareEquiv, UniformSpace.Completion.instMetricSpace, UniformSpace.Completion.coe_isometry, Real.equivCauchy, Padic, UniformSpace.Completion.instNormedSpace, UniformSpace.Completion.innerProductSpace, TopologicalSpace.IsCompletelyMetrizableSpace, PolishSpace, IsUniformGroup, Cauchy |
| Q193756 | Complex analysis | DifferentiableOn, deriv, DifferentiableOn.analyticOnNhd, MeromorphicOn, differentiableAt_complex_iff_differentiableAt_real, AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq, Conformal, ConformalAt, IsConformalMap, Complex.circleIntegral_eq_zero_of_differentiable_on_off_countable, Complex.circleIntegral_sub_inv_smul_of_differentiable_on_off_countable, Differentiable.apply_eq_apply_of_bounded, Complex.isAlgClosed |
| Q381040 | Complex conjugate | Complex.instStarRing, Complex.mul_conj, Polynomial.aeval_conj, starRingEnd, Complex.conj_eq_iff_im, Complex.norm_conj, InvolutiveStar.star_involutive, Complex.inv_def, Complex.exp_conj, Complex.conjAe, Matrix.conjTranspose, ContinuousLinearMap.adjoint, CStarAlgebra, Quaternion.instStarRing, StarMul.star_mul |
| Q11567 | Complex number | Complex, Complex.re, Complex.I, Complex.instAdd, Complex.instMul, Complex.I_sq, Complex.instField, starRingEnd, Complex.conj_conj, Complex.conj_eq_iff_real, Complex.normSq, Complex.norm_def, Complex.dist_eq, Circle, Complex.inv_def, Complex.arg, Complex.arg_mem_Ioc, Complex.norm_mul_cos_add_sin_mul_I, Complex.cos_add_sin_mul_I_pow, Complex.isAlgClosed, Polynomial, Complex.instCompleteSpace, norm_add_le, Complex.exp, Complex.exp_mul_I, Complex.exp_pi_mul_I, Complex.log, Complex.log_im, Complex.cpow, Complex.sin, AnalyticOn, differentiableAt_complex_iff_differentiableAt_real, AnalyticOnNhd.eqOn_of_preconnected_of_frequently_eq, MeromorphicAt, IsAlgebraic, GaussianInt, riemannZeta, Module.End.exists_eigenvalue, Matrix.IsHermitian, Matrix.unitaryGroup, VectorFourier.fourierIntegral, Quaternion, Rat.AbsoluteValue.equiv_real_or_padic, Padic, Complex.finrank_real_complex, Complex.instAlgebraOfReal |
| Q328998 | Complex plane | Complex, Complex.equivRealProdAddHom, Complex.arg_mul_coe_angle, Complex.rotation, Complex.re, Complex.polarCoord, Complex.arg, instInnerProductSpaceRealComplex, stereographic, OnePoint, MeromorphicOn, Complex.not_differentiableAt_Gamma_neg_nat |
| Q1148456 | Computable function | Computable, Nat.Partrec, ComputablePred, REPred, Language, Nat.Primrec.add, Computable.comp, ack, ComputableIn |
| Q205084 | Computational complexity theory | Language, Turing.TM2ComputableInPolyTime, Turing.TM0.Machine, Asymptotics.IsBigO |
| Q830340 | Computer algebra system | fderiv, Matrix.inv, EuclideanDomain.gcd, MvPolynomial.schwartz_zippel_sup_sum, ZMod.chineseRemainder, Polynomial.derivative, MvPolynomial, Real.sin, Real.exp, Real, Int, Complex, IsAlgebraic, Rat |
| Q1575634 | Concrete category | CategoryTheory.ConcreteCategory, CategoryTheory.forget, PartialFun, CategoryTheory.SingleObj, Preorder.smallCategory, CategoryTheory.RelCat, CategoryTheory.Cat |
| Q772232 | Conditional expectation | MeasureTheory.condExpL2, MeasureTheory.ae_eq_condExp_of_forall_setIntegral_eq, MeasureTheory.condExp, MeasureTheory.rnDeriv_ae_eq_condExp, Measurable.exists_eq_measurable_comp, ProbabilityTheory.condExpKernel, ProbabilityTheory.condExp_ae_eq_integral_condExpKernel, MeasureTheory.condExp_indep_eq, MeasureTheory.condExp_of_stronglyMeasurable, MeasureTheory.condExp_mul_of_stronglyMeasurable_left, MeasureTheory.integral_condExp, MeasureTheory.condExp_condExp_of_le, MeasureTheory.martingale_condExp, MeasureTheory.condExp_add, MeasureTheory.condExp_nonneg, MeasureTheory.condExp_mono, ConvexOn.map_condExp_le, ProbabilityTheory.condVar, ProbabilityTheory.condVar_ae_eq_condExp_sq_sub_sq_condExp, ProbabilityTheory.integral_condVar_add_variance_condExp, MeasureTheory.Integrable.tendsto_ae_condExp, MeasureTheory.inner_condExpL2_left_eq_right |
| Q327069 | Conditional probability | ProbabilityTheory.cond, ProbabilityTheory.cond_apply, ProbabilityTheory.sum_meas_smul_cond_fiber, ProbabilityTheory.indepSet_iff_measure_inter_eq_mul, ProbabilityTheory.CondIndepSet, ProbabilityTheory.cond_eq_inv_mul_cond_mul, ProbabilityTheory.cond_add_cond_compl_eq |
| Q319141 | Conjecture | FermatLastTheorem, RiemannHypothesis |
| Q1353233 | Conjugacy class | IsConj, ConjClasses, Subgroup.Normal, MulAut.conj, Sylow.isPretransitive_of_finite, isConj_iff, IsConj.setoid, ConjClasses.mk_bijOn, SemiconjBy.orderOf_eq, IsConj.pow, ConjAct.orbit_eq_carrier_conjClasses, MulAction.orbitEquivQuotientStabilizer, ConjClasses.card_carrier, Group.nat_card_center_add_sum_card_noncenter_eq_card, IsPGroup.center_nontrivial, IsPGroup.commutative_of_card_eq_prime_sq, card_comm_eq_card_conjClasses_mul_card, Subgroup.equivSMul |
| Q1491995 | Connected space | ConnectedSpace, IsConnected, connectedComponentSetoid, isPreconnected_sUnion, connectedComponent, ConnectedComponents, connectedComponent_disjoint, isClosed_connectedComponent, Rat.instTotallyDisconnectedSpace, connectedComponent_subset_iInter_isClopen, TotallyDisconnectedSpace, TotallySeparatedSpace, TotallySeparatedSpace.totallyDisconnectedSpace, isConnected_Icc, Convex.isConnected, isPathConnected_compl_singleton_of_one_lt_rank, Real.instPathConnectedSpace, Path, PathConnectedSpace, IsPathConnected.subset_pathComponent, PathConnectedSpace.connectedSpace, isPreconnected_iff_ordConnected, locallyConnectedSpace_iff_connectedComponentIn_open, LocPathConnectedSpace, IsOpen.isConnected_iff_isPathConnected, IsPreconnected.union, IsConnected.image, instLocallyConnectedSpace, pathConnectedSpace_iff_connectedSpace, IsConnected.closure, isOpen_connectedComponent, biUnion_connectedComponent_pathComponent_eq, Quotient.instConnectedSpace, instConnectedSpaceForall, IsOpen.locallyConnectedSpace, ChartedSpace.locPathConnectedSpace, PreirreducibleSpace.preconnectedSpace, SimplyConnectedSpace.instPathConnectedSpace, ContractibleSpace.instPathConnectedSpace |
| Q338047 | Context-free grammar | ContextFreeGrammar, ContextFreeGrammar.language, Language.IsContextFree, Symbol.nonterminal, Symbol.terminal, ContextFreeRule, ContextFreeGrammar.initial, ContextFreeGrammar.Produces, ContextFreeRule.Rewrites, ContextFreeGrammar.Derives |
| Q170058 | Continuous function | Continuous, Metric.tendsto_nhds, UniformContinuous, ScottContinuous, ContinuousAt, ContinuousOn, Polynomial.continuous, continuous_of_discreteTopology, continuousAt_of_not_accPt, SeqContinuous, Metric.continuous_iff, Oscillation.eq_zero_iff_continuousAt, Continuous.comp, Real.continuous_sin, Real.continuous_exp, Real.continuousOn_log, Real.continuous_sinc, ContinuousAt.preimage_mem_nhds, intermediate_value_Icc, intermediate_value_Ioo, IsCompact.exists_isMinOn, Differentiable.continuous, ContDiff, ContinuousOn.intervalIntegrable, tendsto_pi_nhds, TendstoUniformly.continuous, ContinuousWithinAt, continuousAt_iff_continuous_left_right, LowerSemicontinuous, UpperSemicontinuous, MetricSpace, LinearMap.continuous_iff_isClosed_ker, UniformContinuous.continuous, CompactSpace.uniformContinuous_of_continuous, HolderWith, LipschitzWith, IsPicardLindelof.exists_eq_forall_mem_Icc_hasDerivWithinAt, TopologicalSpace, continuous_iff_isClosed, continuous_iff_continuousAt, SequentialSpace, continuous_iff_seqContinuous, continuous_iff_image_closure_subset_closure_image, TopologicalSpace.mkOfClosure, continuousAt_iff_ultrafilter, IsCompact.image, IsConnected.image, IsPathConnected.image, IsLindelof.image, TopologicalSpace.IsSeparable.image, continuous_id_iff_le, IsOpenMap, Homeomorph, Continuous.homeoOfEquivCompactToT2, TopologicalSpace.coinduced, instTopologicalSpaceQuotient, TopologicalSpace.induced, instTopologicalSpaceSubtype, IsDenseInducing.extend, BoundedContinuousFunction.exists_extension_norm_eq_of_isClosedEmbedding, exists_extension_norm_eq, Continuous.ext_on, ScottContinuousOn, Continuous.add, Continuous.inv₀, continuous_const, continuous_id, Metric.continuousAt_iff, TopologicalSpace.le_def, continuousOn_inv₀, Real.continuousOn_tan, oscillation, nhds, DirectedOn, Topology.scott |
| Q208416 | Continuum hypothesis | Cardinal.sum_lt_prod, Ordinal.cof, Cardinal.eq, Equiv, Cardinal.mkRat, Set.Countable, Cardinal.aleph0_lt_continuum, Cardinal.cantor, Cardinal.mk_real, Classical.choice, Cardinal.aleph_one_le_iff, Cardinal.aleph, Cardinal.power_le_power_left |
| Q578985 | Convergence of random variables | MeasureTheory.TendstoInDistribution, MeasureTheory.limsup_measure_closed_le_iff_liminf_measure_open_ge, MeasureTheory.TendstoInDistribution.continuous_comp, MeasureTheory.ProbabilityMeasure.tendsto_iff_tendsto_charFun, MeasureTheory.LevyProkhorov.eq_convergenceInDistribution, MeasureTheory.TendstoInMeasure, MeasureTheory.TendstoInMeasure.tendstoInDistribution, Filter.Eventually, MeasureTheory.tendstoInMeasure_of_tendsto_ae, Filter.Tendsto, MeasureTheory.eLpNorm, MeasureTheory.tendstoInMeasure_of_tendsto_eLpNorm, MeasureTheory.eLpNorm_le_eLpNorm_of_exponent_le, MeasureTheory.AEEqFun.tendsto_ae_unique, MeasureTheory.TendstoInMeasure.exists_seq_tendsto_ae, MeasureTheory.TendstoInDistribution.add_of_tendstoInMeasure_const, MeasureTheory.TendstoInDistribution.prodMk_of_tendstoInMeasure_const, MeasureTheory.tendsto_integral_filter_of_dominated_convergence, MeasureTheory.tendstoInMeasure_iff_tendsto_Lp_finite |
| Q193657 | Convex set | Convex, convexHull, ConvexOn, convex_iff_add_mem, Convex.affine_image, Convex.isPathConnected, StrictConvex, AbsConvex, convex_iff_ordConnected, Convex.sum_mem, Finset.centerMass, convex_empty, convex_sInter, DirectedOn.convex_sUnion, exists_extension_norm_eq, IsExtreme, Set.extremePoints, closure_convexHull_extremePoints, StrictConvexSpace.extremePoints_closedBall_eq_sphere, Convex.closure, Convex.add_smul, convexHull_min, Set.add, Set.addMonoid, convexHull_add, convexHull_sum, convexHullAddMonoidHom, IsCompact.add, IsClosed.add_left_of_isCompact, StarConvex, Convex.starConvex, Set.OrdConnected |
| Q210857 | Convolution | MeasureTheory.convolution, MeasureTheory.convolution_eq_swap, MeasureTheory.posConvolution, DiscreteConvolution.convolution, DiscreteConvolution.convolution_comm, Polynomial.coeff_mul, HasCompactSupport.convolution, HasCompactSupport.convolutionExists_left, MeasureTheory.Integrable.integrable_convolution, SchwartzMap.convolution, MeasureTheory.Measure.conv, MeasureTheory.convolution_flip, MeasureTheory.convolution_assoc, MeasureTheory.ConvolutionExists.distrib_add, MeasureTheory.convolution_smul, MeasureTheory.integral_convolution, HasCompactSupport.hasDerivAt_convolution_right, HasCompactSupport.hasFDerivAt_convolution_right, Real.fourier_mul_convolution_eq, MeasureTheory.mconv_withDensity_eq_mlconvolution, ProbabilityTheory.IndepFun.map_add_eq_map_conv_map₀, LinearMap.convMul |
| Q11210 | Coordinate system | polarCoord, AffineBasis.coord, ChartedSpace, ChartedSpace.atlas, IsManifold |
| Q104752 | Coprime integers | Nat.Coprime, Nat.totient, Nat.Coprime.isCoprime, ZMod.unitOfCoprime, Nat.chineseRemainder, Nat.Coprime.lcm_eq_mul, Nat.ModEq.cancel_left_div_gcd, IsCoprime.mul_right, Nat.Prime.dvd_mul, IsCoprime.pow, IsCoprime.dvd_of_dvd_mul_right, Pairwise, Nat.coprime_fermatNumber_fermatNumber, hasSum_zeta_two, IsCoprime, Ideal.isCoprime_iff_add, Ideal.mul_eq_inf_of_coprime, Ideal.quotientInfRingEquivPiQuotient |
| Q186290 | Correlation | ProbabilityTheory.IndepFun.covariance_eq_zero, ProbabilityTheory.HasGaussianLaw.indepFun_of_covariance_eq_zero, ProbabilityTheory.covariance |
| Q1713076 | Cotangent space | IsLocalRing.CotangentSpace, mfderiv |
| Q66707394 | Countable set | Set.Countable, Denumerable, Function.cantor_surjective, Classical.axiomOfChoice, Cardinal.mk, countable_iff_exists_injective, Cardinal.aleph0, countable_iff_exists_surjective, Uncountable, Infinite, Equiv, Cardinal.eq, Cardinal.not_countable_real, Cardinal.mk_real, Cardinal.cantor, Set.Finite.countable, Set.countable_infinite_iff_nonempty_denumerable, Denumerable.prod, Set.prod, Algebraic.countable, Subtype.countable, Set.powerset, Set.Countable.mono, Set.Countable.prod, Denumerable.int, Set.Countable.union, Set.countable_iUnion, Denumerable.denumerableList, Set.countable_setOf_finite_subset, Function.Injective.countable, IsWellOrder, Ordinal, FirstOrder.Language.exists_elementarySubstructure_card_eq, Function.Injective, Nat, Function.Surjective, Rat, Real, Set.Finite |
| Q201984 | Covariance | ProbabilityTheory.covariance, ProbabilityTheory.covariance_eq_sub, ProbabilityTheory.covariance_self, ProbabilityTheory.covariance_add_left, ProbabilityTheory.covariance_sum_sum', ProbabilityTheory.IndepFun.covariance_eq_zero, ProbabilityTheory.HasGaussianLaw.iIndepFun_of_covariance_eq_zero, ProbabilityTheory.isPosSemidef_covarianceBilin |
| Q3555165 | Covariance and contravariance of vectors | Module.Dual, Module.dualPairing, Module.Basis.toMatrix, Module.Basis.repr, Module.Basis.toMatrix_mulVec_repr, Module.Basis.dualBasis, Module.Basis.coord, TangentSpace, LinearMap.BilinForm.toDual, LinearMap.BilinForm.dualBasis, LinearMap.BilinForm.dualBasis_repr_apply, InnerProductSpace.toDualMap, LinearMap.BilinForm.apply_dualBasis_left, LinearMap.BilinForm.dualBasis_dualBasis_flip, Module.Basis, LinearMap.BilinForm.toMatrix, LinearMap.BilinForm.Nondegenerate, Matrix.one_apply |
| Q2287715 | Covariant derivative | CovariantDerivative, IsCovariantDerivativeOn, IsCovariantDerivativeOn.congr_of_eventuallyEq, IsCovariantDerivativeOn.leibniz |
| Q332648 | Covering space | IsCoveringMap, IsFiberBundle.isCoveringMap, AddCircle.isCoveringMap_coe, AddCircle.isAddQuotientCoveringMap_zsmul, IsCoveringMap.isLocalHomeomorph, IsCoveringMap.existsUnique_continuousMap_lifts_of_range_le, IsCoveringMap.liftPath, IsCoveringMap.monodromy_bijective, IsCoveringMap.injective_path_homotopic_map, ProperlyDiscontinuousSMul, IsCoveringMap.liftHomotopy |
| Q7874246 | Coxeter group | CoxeterMatrix.Group, CoxeterSystem, CoxeterSystem.simple_mul_simple_self, CoxeterMatrix, CoxeterSystem.length, CoxeterSystem.IsReduced, CoxeterSystem.lengthParity |
| Q178192 | Cross product | crossProduct, InnerProductGeometry.norm_ofLp_crossProduct, cross_anticomm, dot_self_cross, crossProduct_ne_zero_iff_linearIndependent, cross_self, cross_apply, triple_product_eq_det, jacobi_cross, cross_cross_eq_smul_sub_smul', cross_dot_cross |
| Q812880 | Cube | SimpleGraph.boxProd, EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two |
| Q203565 | Cubic equation | Cubic, num_dvd_of_is_root, Cubic.discr_eq_prod_three_roots, Cubic.discr, Polynomial.aeval_conj, Cubic.discr_ne_zero_iff_roots_nodup, Polynomial.one_lt_rootMultiplicity_iff_isRoot |
| Q206310 | Curl (mathematics) | extDeriv, extDeriv_extDeriv |
| Q975734 | Curry–Howard correspondence | CategoryTheory.CartesianMonoidalCategory, CategoryTheory.MonoidalClosed.curry, CategoryTheory.MonoidalClosed |
| Q161973 | Curve | Path, eVariationOn, BoundedVariationOn, HasUnitSpeedOn, LipschitzWith.locallyBoundedVariationOn, WeierstrassCurve.IsElliptic |
| Q245462 | Cyclic group | IsCyclic, intCyclicAddEquiv, IsCyclic.commGroup, isSimpleGroup_of_prime_card, Subgroup.zpowers, ZMod, instIsAddCyclicInt, ZMod.instIsAddCyclic, ZMod.isUnit_iff_coprime, ZMod.instField, ZMod.isCyclic_units_iff, isCyclic_subgroup_units, rootsOfUnity, rootsOfUnity.isCyclic, FiniteField.instIsCyclicAlgEquivOfFinite, FiniteField.Extension, Subgroup.isCyclic, CommGroup.is_simple_iff_prime_card, IsCyclic.isMulCommutative, AddCommGroup.equiv_free_prod_directSum_zmod, IsCyclic.card_orderOf_eq_totient, isCyclic_of_card_pow_eq_one_le, ZMod.addOrderOf_coe, ZMod.chineseRemainder, isCyclic_of_prime_card, ZMod.AddAutEquivUnits |
| Q190556 | De Moivre's formula | Complex.cos_add_sin_mul_I_pow, Complex.exp_mul_I, Complex.cos_three_mul, Polynomial.Chebyshev.T_complex_cos |
| Q177571 | Decision theory | ProbabilityTheory.strong_law_ae, ProbabilityTheory.cond_eq_inv_mul_cond_mul |
| Q29175 | Derivative | fderiv, DifferentiableAt, deriv, deriv_pow_field, DifferentiableAt.continuousAt, not_differentiableAt_abs_zero, fderiv_comp, Real.deriv_exp, Real.deriv_sin, Real.deriv_arcsin, fderiv_const, fderiv_add, deriv_mul, deriv_div, intervalIntegral.integral_eq_sub_of_hasDerivAt, iteratedDeriv, ContDiff, CPolynomialOn.contDiffOn, gradient, lineDeriv, HasFDerivAt.hasLineDerivAt, mfderiv, differentiableWithinAt_complex_iff_differentiableWithinAt_real, Derivation |
| Q178546 | Determinant | Matrix.det, Matrix.isUnit_iff_isUnit_det, Matrix.det_mul, Matrix.det_conj, Matrix.det_fin_two, Matrix.det_one, Matrix.det_zero_of_row_eq, Matrix.det_updateCol_smul, Matrix.det_fin_three, Equiv.Perm, Equiv.Perm.sign, Matrix.det_apply, Matrix.detRowAlternating, Matrix.det_smul, Matrix.det_permute, Matrix.det_eq_zero_of_not_linearIndependent_cols, Matrix.det_updateCol_add_smul_self, Matrix.det_of_upperTriangular, Matrix.det_transpose, Matrix.det_nonsing_inv, Matrix.GeneralLinearGroup.det, Matrix.det_succ_row, Matrix.adjugate, Matrix.mul_adjugate, Matrix.det_fromBlocks_zero₂₁, Matrix.det_one_add_mul_comm, Matrix.det_eq_prod_roots_charpoly, Matrix.charpoly, Matrix.cramer, Polynomial.resultant, Module.Basis.orientation_eq_iff_det_pos, Matrix.linearIndependent_cols_of_det_ne_zero, MeasureTheory.integral_image_eq_integral_abs_det_fderiv_smul, HasStrictFDerivAt.localInverse, LinearMap.det, ExteriorAlgebra.exteriorPower, Matrix.permanent, Algebra.norm, Matrix.GeneralLinearGroup, Matrix.SpecialLinearGroup, RingHom.map_det, Matrix.aeval_self_charpoly, Matrix.trace_eq_sum_roots_charpoly, Matrix.nonsing_inv_apply, MeasureTheory.Measure.addHaar_image_linearMap, Complex.isAlgClosed, Module.End.hasEigenvalue_iff_isRoot_charpoly, NormedSpace.exp, QuotientGroup.quotientKerEquivOfSurjective |
| Q1058314 | Diffeomorphism | Diffeomorph, Diffeomorph.toHomeomorph, IsLocalDiffeomorph, Manifold.IsImmersion, fderiv |
| Q628007 | Difference engine | shift_eq_sum_fwdDiff_iter, Polynomial.fwdDiff_iter_degree_eq_factorial, AnalyticAt, taylorWithin, Lagrange.interpolate |
| Q3552958 | Differentiable manifold | ChartedSpace, HasGroupoid, StructureGroupoid.maximalAtlas, IsManifold, contDiffGroupoid_zero_eq, MDifferentiableAt, TangentSpace, mfderiv, SmoothPartitionOfUnity.IsSubordinate, SmoothPartitionOfUnity.exists_isSubordinate, ContMDiff, TangentBundle, tangentMap, IsRiemannianManifold, LieGroup, StructureGroupoid, ContMDiffMap |
| Q149999 | Differential calculus | deriv, HasDerivAt, deriv_pow, hasFDerivAt_iff_isLittleO, IsLocalExtr.deriv_eq_zero, exists_deriv_eq_zero, exists_deriv_eq_slope, is_const_of_deriv_eq_zero, taylor_mean_remainder_lagrange, isLocalMax_of_deriv, isLocalMin_of_deriv_deriv_pos, IsLocalExtr.fderiv_eq_zero, ImplicitFunctionData.implicitFunction, HasStrictFDerivAt.to_localInverse |
| Q11214 | Differential equation | InnerProductSpace.HarmonicAt |
| Q1047080 | Differential form | Orientation.volumeForm, extDeriv, lineDeriv, fderiv, extDeriv_apply, AlternatingMap, MultilinearMap.alternatization, extDeriv_extDeriv, mfderiv |
| Q188444 | Differential geometry | IsRiemannianManifold, LieGroup, GroupLieAlgebra |
| Q2502381 | Differential geometry of surfaces | ContDiffOn, EuclideanSpace.instIsManifoldSphere, VectorField.mlieBracket, Bundle.RiemannianMetric, Manifold.pathELength_comp_of_monotoneOn, EuclideanGeometry.law_cos |
| Q1058681 | Differential operator | gradient, ContinuousLinearMap.adjoint, MeasureTheory.L2.inner_def, LinearPMap.IsFormalAdjoint, LinearMap.IsSymmetric, deriv_add |
| Q1227061 | Diophantine approximation | Liouville.exists_pos_real_of_irrational_root, transcendental_liouvilleNumber, Real.infinite_rat_abs_sub_lt_one_div_den_sq_of_irrational, Liouville |
| Q209675 | Dirac delta function | TemperedDistribution.delta, MeasureTheory.Measure.dirac, MeasureTheory.mutuallySingular_dirac, Distribution.delta, Distribution.delta_apply, ContDiffBump.normed, poissonKernel, TemperedDistribution.fourier_delta_zero, Real.tsum_eq_tsum_fourier, Orthonormal |
| Q272621 | Dirac equation | Representation |
| Q1195339 | Directed acyclic graph | SimpleGraph.hasse, Quiver.Arborescence |
| Q20968946 | Discrete calculus | slope, BoxIntegral.integralSum, intervalIntegral.integral_eq_sub_of_hasDerivAt, Finset.sum_range_sub, fwdDiff, fwdDiff_const, fwdDiff_add, fwdDiff_smul, Geometry.SimplicialComplex, AlgebraicTopology.AlternatingFaceMapComplex.objD, HomologicalComplex.cycles, HomologicalComplex.d_comp_d, ChainComplex, HomologicalComplex.Hom, CochainComplex, groupCohomology.cocycles, fwdDiff_iter_eq_sum_shift, Affine.Simplex, Module.Dual |
| Q2878 | Discrete Fourier transform | ZMod.dft, ZMod.dft_apply, ZMod.invDFT_apply, ZMod.dft_comp_neg, ZMod.invDFT_apply' |
| Q121416 | Discrete mathematics | peirce |
| Q126017 | Distance | EuclideanSpace.dist_eq, PiLp.dist_eq_of_L1, dist_pi_def, EuclideanSpace.dist_sq_eq, InformationTheory.klDiv, SimpleGraph.dist, MetricSpace, Metric.hausdorffDist, Metric.NonemptyCompacts.instMetricSpace, eVariationOn |
| Q865811 | Distribution (mathematical analysis) | Distribution, TestFunction, Distribution.delta, TemperedDistribution.toTemperedDistribution_dirac_eq_delta, Distribution.lineDerivCLM, HasCompactSupport, MeasureTheory.LocallyIntegrable, ae_eq_of_integral_contDiff_smul_eq, LineDeriv.iteratedLineDerivOp, Distribution.IsVanishingOn, Distribution.dsupport, TemperedDistribution, SchwartzMap, SchwartzMap.seminorm, SchwartzMap.fourierTransformCLM, TemperedDistribution.derivCLM, Function.HasTemperateGrowth.toTemperedDistribution, TemperedDistribution.instFourierTransform, FourierTransform.fourierCLE |
| Q187959 | Distributive property | Distrib, left_distrib, LeftDistribClass, RightDistribClass, add_div, Ring, Finset.sum_mul_sum, mul_add, Matrix.mul_add, Ordinal.leftDistribClass, crossProduct, Set.inter_union_distrib_left, or_and_left, max_min_distrib_left, max_add_add_left, add_mul_add, Semiring, Algebra, and_or_left, DistribLattice, BooleanRing.toBooleanAlgebra, mul_inv_rev, imp_and |
| Q906520 | Divergent series | Summable.tendsto_atTop_zero, Real.not_summable_one_div_natCast, HasSum, summable_norm_iff |
| Q1226939 | Division (mathematics) | Nat.div_add_mod, div_eq_mul_inv, EuclideanDomain, Polynomial.instEuclideanDomain, DivisionRing, IsUnit, QuotientGroup.Quotient.group, add_div, ZMod.instField, Int.euclideanDomain, Int.ediv, Dvd.dvd, Rat.instField, Real.instField, Complex.inv_def, Polynomial.div, Finite.isField_of_domain, deriv_div, Nat.mod_lt, Rat, Rat.div_def, Polynomial.divByMonic, IsCancelMul, IsDomain, Subsingleton |
| Q848539 | Division by zero | div_zero, div_eq_mul_inv, Filter.Tendsto, slope, tendsto_inv_nhdsGT_zero, Filter.Tendsto.div, EReal, Rat.isFractionRing, IsLocalization.subsingleton |
| Q50708 | Divisor | semigroupDvd, dvd_def, Even, dvd_trans, Associated, IsCoprime.dvd_of_dvd_mul_right, Nat.Prime.dvd_mul, Nat.properDivisors, Nat.Prime, Nat.divisors_prime_pow, Nat.Perfect, ArithmeticFunction.isMultiplicative_sigma, ArithmeticFunction.sigma_one_apply, Nat.card_divisors, Associates.instLattice, one_dvd, dvd_refl, dvd_add, Nat.primeFactorsList_unique, ArithmeticFunction.sigma, ArithmeticFunction.IsMultiplicative, Nat.gcd, Nat.lcm, Nat.Coprime, Dvd, Nat.divisors, dvd_iff_exists_eq_mul_left, associated_of_dvd_dvd |
| Q181365 | Dot product | dotProduct, InnerProductGeometry.cos_angle_mul_norm_mul_norm, real_inner_self_eq_norm_mul_norm, add_dotProduct, InnerProductSpace, EuclideanSpace.basisFun, EuclideanSpace.inner_eq_star_dotProduct, dotProduct_comm, smul_dotProduct, Submodule.mem_orthogonal_singleton_iff_inner_right, HasDerivAt.inner, InnerProductGeometry.norm_sub_sq_eq_norm_sq_add_norm_sq_sub_two_mul_norm_mul_norm_mul_cos_angle, triple_product_eq_det, InnerProductSpace.conj_inner_symm, InnerProductSpace.norm_sq_eq_re_inner, MeasureTheory.L2.innerProductSpace, TensorProduct.instInnerProductSpace, InnerProductSpace.Core.norm_eq_sqrt_re_inner, InnerProductGeometry.cos_angle, EuclideanSpace |
| Q752487 | Dual space | Module.Dual, StrongDual, Module.Dual.eval, Module.Basis.dualBasis, Module.Basis.dualBasis_apply_self, lift_rank_lt_rank_dual, rank_dual_eq_card_dual_of_aleph0_le_rank, LinearMap.BilinForm.toDual, Module.evalEquiv, LinearMap.dualMap, Module.Dual.transpose_apply, LinearMap.toMatrix_transpose, Submodule.dualAnnihilator, Submodule.dualAnnihilator_sup_eq, Submodule.dualAnnihilator_gc, Submodule.dualQuotEquivDualAnnihilator, Module.dualProdDualEquivDual, LinearMap.toContinuousLinearMap, ContinuousLinearMap.toNormedAddCommGroup, WeakDual, InnerProductSpace.toDual, RealRMK.integral_rieszMeasure, NormedSpace.inclusionInDoubleDual, NormedSpace.inclusionInDoubleDualLi, Module.Dual.transpose_comp, Submodule.dualAnnihilator_anti |
| Q1755512 | Duality (mathematics) | LinearMap.BilinMap, Module.Dual, Set.compl, compl_compl, Set.compl_subset_compl, isClosed_compl_iff, closure_compl, isOpen_iUnion, PointedCone.dual, PointedCone.subset_dual_dual, PointedCone.dual_antitone, Module.evalEquiv, InnerProductSpace.toDual, IntermediateField.fixingSubgroup, FixedPoints.intermediateField, IsGalois.intermediateFieldEquivSubgroup, OrderDual, Matroid.dual, not_exists, compl_sup, compl_inf, Set.compl_union, Module.Dual.eval, Module.eval_ker, Module.IsReflexive, Basis.linearEquiv_dual_iff_finiteDimensional, InnerProductSpace, PontryaginDual, CategoryTheory.Category.opposite, CategoryTheory.Limits.HasProducts, CategoryTheory.Limits.limit, CategoryTheory.Adjunction, CategoryTheory.Limits.colimConstAdj, gelfandStarTransform, AlgebraicGeometry.AffineScheme.equivCommRingCat, GaloisConnection, TopologicalSpace.Opens.instFrame, PontryaginDual.instDiscreteTopology, VectorFourier.fourierIntegral, Real.fourier_bilin_convolution_eq, LinearMap.IsPerfPair |
| Q380679 | Dynamic programming | Matrix.mul_assoc |
| Q638328 | Dynamical system | Flow.orbit, MeasureTheory.Conservative.measure_mem_forall_ge_image_notMem_eq_zero, Flow, Flow.fromIter, Flow.toFun, MeasureTheory.MeasurePreserving, nonempty_omegaLimit, Flow.toAddAction, IsInvariant, IsPicardLindelof.exists_eq_forall_mem_Icc_eq_picard, Nat.iterate, StoneCech, OnePoint, Function.IsFixedPt, Function.IsPeriodicPt, MeasureTheory.Conservative, omegaLimit, birkhoffAverage, AddAction |
| Q82435 | E (mathematical constant) | ProbabilityTheory.gaussianReal, numDerangements_tendsto_inv_e, Stirling.tendsto_stirlingSeq_sqrt_pi, Real.hasDerivAt_exp, NormedSpace.exp_eq_tsum_div, Real.exp_log, Real.add_one_le_exp, Complex.exp_mul_I, Complex.exp_pi_mul_I, Complex.cos_add_sin_mul_I_pow, Complex.cos, Real.exp_one_near_20, ProbabilityTheory.gaussianPDFReal, integral_gaussian, Stirling.factorial_isEquivalent_stirling, Real.exp |
| Q190524 | Eigenvalues and eigenvectors | Module.End.HasEigenvector, Module.End.HasEigenvalue, LinearMap.spectrum_toMatrix, Module.End.mem_eigenspace_iff, SameRay, Module.End.eigenspace_def, Module.End.hasEigenvalue_iff_isRoot_charpoly, LinearMap.charpoly, LinearMap.charpoly_natDegree, spectrum, spectralRadius, Module.End.eigenspace, LinearMap.finrank_eigenspace_le, Module.End.trace_eq_sum_roots_charpoly_of_splits, Module.End.det_eq_prod_roots_charpoly_of_splits, Module.End.HasEigenvalue.pow, spectrum.zero_notMem_iff, Matrix.IsHermitian.eigenvalues_mem_spectrum_real, Matrix.PosSemidef.eigenvalues_nonneg, spectrum.norm_eq_one_of_unitary, Matrix.charpoly_transpose, LinearMap.IsSymmetric.hasEigenvalue_iSup_of_finiteDimensional, spectrum_diagonal, Module.End.eigenspaces_iSupIndep, Module.End.eigenspace_mem_invtSubmodule, LieModule.weightSpace, Module.End.eigenvectors_linearIndependent, Module.End.instFintypeEigenvalues, spectrum.inv_mem_iff, Matrix.IsHermitian.eigenvalues, Module.End.genEigenspace |
| Q211294 | Elementary algebra | pow_zero, pow_one, add_comm, left_distrib, EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two, mul_lt_mul_of_neg_left, eq_equivalence, Eq.subst, lt_trans, ge_iff_le, mul_eq_zero, quadratic_eq_zero_iff, Real.rpow_inv_natCast_pow |
| Q268493 | Elliptic curve | WeierstrassCurve.Affine.Nonsingular, WeierstrassCurve.IsShortNF, WeierstrassCurve.Affine.Point.instAddCommGroup, WeierstrassCurve.Affine.Point.neg, WeierstrassCurve.Affine.Point.add, WeierstrassCurve.Affine.Point, WeierstrassCurve.Affine.Point.map, WeierstrassCurve.Affine.slope_of_X_ne, WeierstrassCurve.Affine.negY, WeierstrassCurve.Affine.slope_of_Y_ne, WeierstrassCurve.Affine.slope, WeierstrassCurve.LFunction, WeierstrassCurve.exists_variableChange_isShortNF, WeierstrassCurve.exists_variableChange_isCharThreeNF, WeierstrassCurve.exists_variableChange_isCharTwoNF, PeriodPair.derivWeierstrassP_sq, PeriodPair.weierstrassP_add_coe, WeierstrassCurve.exists_variableChange_of_j_eq, PeriodPair.g₂ |
| Q938102 | Elliptic function | PeriodPair.lattice, ZSpan.fundamentalDomain, PeriodPair.weierstrassP, PeriodPair.weierstrassP_neg, PeriodPair.derivWeierstrassP_neg, PeriodPair.derivWeierstrassP_sq |
| Q1332450 | Elliptic geometry | Projectivization.equivSubmodule |
| Q226183 | Empty set | Set.instEmptyCollection, Set.Nonempty, Set.eq_empty_iff_forall_notMem, Set.powerset_empty, Set.union_empty, Set.forall_mem_empty, Set.empty_subset, Finset.sum_empty, upperBounds_empty, sSup_empty, isOpen_empty, IndiscreteTopology, closure_empty, CategoryTheory.Limits.Types.isInitialPEmpty, TopCat.isInitialPEmpty, Set.disjoint_iff_inter_eq_empty |
| Q204570 | Entropy (information theory) | Real.binEntropy, Real.negMulLog_zero, InformationTheory.klDiv |
| Q842346 | Equality (mathematics) | Eq, Ne, Eq.refl, Eq.symm, Eq.trans, Eq.subst, congrArg, BEq, funext, rfl, Set.ext, setOf, Set.ext_iff, Prod.ext_iff, FP.Float, Equivalence, Setoid.isPartition_classes, Setoid.bot_def, Con, CategoryTheory.Iso, Equiv, MulEquiv, zmodMulEquivOfGenerator, LinearEquiv.nonempty_equiv_iff_rank_eq, EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two, EuclideanSpace.volume_ball, Similar |
| Q1879820 | Equation solving | Polynomial.IsRoot, Set.preimage, Dioph, Function.invFun, Polynomial.newtonMap |
| Q1211071 | Equivalence class | Setoid.classes, Setoid.mem_classes, Setoid.quotientEquivClasses, Setoid, Quotient.mk_surjective, Quotient.out, Setoid.isPartition_classes, Setoid.Partition.orderIso, Quotient.eq, ZMod, Setoid.bot_def, Quotient.lift, Setoid.ker, Quotient.map, instTopologicalSpaceQuotient, QuotientGroup.Quotient.group, MulAction.orbitRel, QuotientGroup.instIsTopologicalGroup |
| Q130998 | Equivalence relation | Setoid, eq_equivalence, Setoid.isPartition_classes, Setoid.classes, Relation.Comp, Quotient, Similar, Congruent, Setoid.ker, Int.ModEq, PartialOrder, IsStrictOrder, Preorder, Con, Quotient.mk, Setoid.injective_iff_ker_bot, Setoid.IsPartition, Setoid.Partition.orderIso, Setoid.le_def, Setoid.completeLattice, Setoid.ker_mk_eq, Setoid.sInf_def, Setoid.eqvGen_eq, QuotientGroup.mk |
| Q5498822 | Ergodic theory | MeasureTheory.Conservative.measure_mem_forall_ge_image_notMem_eq_zero, Ergodic, AddCircle.ergodic_add_left, ContinuousLinearMap.tendsto_birkhoffAverage_orthogonalProjection |
| Q172891 | Euclid's Elements | EuclideanGeometry.angle_eq_angle_of_dist_eq, InnerProductGeometry.norm_add_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two, Real.goldenRatio, Orientation.oangle_eq_two_zsmul_oangle_sub_of_norm_eq, EuclideanGeometry.Sphere.angle_eq_pi_div_two_iff_mem_sphere_of_isDiameter, EuclideanGeometry.mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_pi, EuclideanGeometry.Sphere.dist_sq_eq_mul_dist_of_tangent_and_secant, Nat.exists_infinite_primes, geom_sum_eq, Nat.Perfect, irrational_sqrt_intCast_iff_of_nonneg, PythagoreanTriple.isPrimitiveClassified_of_coprime, EuclideanSpace.volume_ball_fin_three, Nat.gcd, InnerProductGeometry.norm_sub_sq_eq_norm_sq_add_norm_sq_sub_two_mul_norm_mul_norm_mul_cos_angle, Nat.Prime.irrational_sqrt |
| Q230848 | Euclidean algorithm | EuclideanDomain.gcd, Nat.gcd_sub_self_left, Int.gcd_eq_gcd_ab, Nat.gcd, Nat.Coprime, Nat.dvd_gcd, Nat.factorization_gcd, Int.gcd_least_linear, Nat.gcd_rec, Nat.gcd_comm, EuclideanDomain.div_add_mod, Int.ediv_emod_unique, Nat.xgcd, EuclideanDomain.gcd_eq_gcd_ab, span_gcd, IsPrincipalIdealRing, Nat.gcd_eq_gcd_ab, Nat.Prime.dvd_mul, Nat.Coprime.mul_right, Nat.factorization_inj, Int.gcd_dvd_iff, ZMod.instField, ZMod.unitOfCoprime, ZMod.chineseRemainder, EuclideanDomain, GenContFract.terminates_iff_rat, Polynomial.instEuclideanDomain, EuclideanDomain.gcd_dvd_left, GaussianInt, PrincipalIdealRing.to_uniqueFactorizationMonoid, Zsqrtd.norm, EuclideanDomain.to_principal_ideal_domain, Zsqrtd, Nat.sum_four_squares |
| Q847073 | Euclidean distance | EuclideanSpace.dist_eq, Real.dist_eq, Complex.dist_eq, EuclideanSpace.norm_eq, dist_comm, dist_pos, dist_triangle, EuclideanGeometry.mul_dist_le_mul_dist_add_mul_dist, lp, EuclideanSpace, PiLp |
| Q162886 | Euclidean geometry | EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two, Nat.exists_infinite_primes, EuclideanGeometry.angle_eq_angle_of_dist_eq, EuclideanGeometry.angle_add_angle_add_angle_eq_pi, EuclideanGeometry.Sphere.angle_eq_pi_div_two_iff_mem_sphere_of_isDiameter, EuclideanGeometry.side_side_side, EuclideanGeometry.similar_of_angle_angle, MeasureTheory.Measure.addHaar_smul, Congruent, Similar, Archimedean, EuclideanSpace.dist_eq, and_not_self_iff, em, Quaternion, EuclideanSpace, EuclideanSpace.equiv, geom_sum_eq, CliffordAlgebra |
| Q116980063 | Euclidean planes in three-dimensional space | parallelepiped |
| Q17295 | Euclidean space | EuclideanSpace, OrthonormalBasis.repr, InnerProductSpace, AddTorsor, Module.finrank, VAdd.vadd, vsub_vadd, AddGroup.instAddTorsor, AffineSubspace, AffineSubspace.direction, AffineSubspace.mk', Submodule.toAffineSubspace, affineSegment, AffineSubspace.Parallel, Inner.inner, EuclideanSpace.norm_eq, EuclideanSpace.dist_eq, dist_triangle, dist_add_dist_eq_iff, PiLp.completeSpace, InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two, Submodule.IsOrtho, EuclideanGeometry.angle, EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two, InnerProductGeometry.angle, abs_real_inner_div_norm_mul_norm_le_one, Orientation.oangle, InnerProductGeometry.angle_smul_left_of_pos, stdOrthonormalBasis, AffineBasis, IsometryEquiv, LinearIsometry.inner_map_map, AffineMap.ofMapMidpoint, AffineIsometryEquiv.vaddConst, AffineIsometryEquiv.instGroup, AffineIsometryEquiv.constVAdd, AffineIsometryEquiv.linearIsometryEquiv, Module.reflection, EuclideanSpace.equiv, Metric.isOpen_iff, Metric.isCompact_iff_isClosed_bounded, ChartedSpace, AffineSpace, Projectivization, TangentSpace |
| Q44528 | Euclidean vector | EuclideanSpace, InnerProductSpace, stdOrthonormalBasis, Pi.add_apply, Eq, Neg.neg, HAdd.hAdd, add_comm, HSub.hSub, SMul.smul, smul_add, Norm.norm, norm_eq_sqrt_re_inner, NormedSpace.normalize, Zero.zero, zero_add, Inner, PiLp.inner_apply, crossProduct, triple_product_eq_det |
| Q751290 | Euler angles | Matrix.specialOrthogonalGroup, Matrix.specialUnitaryGroup |
| Q852973 | Euler characteristic | HomologicalComplex.homologyEulerChar, IncidenceAlgebra.eulerChar |
| Q273023 | Euler's constant | Real.eulerMascheroniConstant, Complex.digamma_one, tendsto_riemannZeta_sub_one_div |
| Q184871 | Euler's formula | Complex.exp_mul_I, Complex.exp_pi_mul_I, Complex.exp, NormedSpace.expSeries_radius_eq_top, Complex.tendsto_one_add_div_pow_exp, Complex.exp_ne_zero, Complex.hasDerivAt_exp, Complex.range_exp_mul_I, Complex.norm_mul_exp_arg_mul_I, Complex.arg, Complex.exp_add, Complex.log, Complex.cos_add_sin_mul_I_pow, Complex.two_cos, Complex.cos, Complex.cos_mul_I, Circle.exp, Complex.exp_eq_one_iff, Quaternion.exp_of_re_eq_zero, Complex.exp_two_pi_mul_I, Real.log_exp, Complex.I, Complex.cos_ofReal_re, Complex.cos_add_sin_I, Complex.norm_def, Complex.conj_I, Complex.exp_log |
| Q204819 | Euler's identity | Complex.exp_pi_mul_I, Complex.I, Real.pi, Complex.exp, Complex.tendsto_one_add_div_pow_exp, Complex.exp_mul_I, Complex.norm_mul_exp_arg_mul_I, Complex.rotation, IsPrimitiveRoot.geom_sum_eq_zero |
| Q193910 | Euler's theorem | Nat.ModEq.pow_totient, Nat.pow_totient_mod, ZMod.pow_totient |
| Q190026 | Euler's totient function | Nat.totient, Nat.totient_mul, ZMod.card_units_eq_totient, Nat.totient_eq_prod_factorization, Nat.totient_eq_mul_prod_factors, ZMod.chineseRemainder, Nat.totient_prime_pow, UniqueFactorizationMonoid.factors_unique, Nat.sum_totient, ArithmeticFunction.moebius, Nat.ModEq.pow_totient, ZMod.pow_card_sub_one_eq_one |
| Q200125 | Expected value | MeasureTheory.integral, MeasureTheory.integral_finset, MeasureTheory.integral_tsum, MeasureTheory.pdf.integral_pdf_smul, MeasureTheory.HasPDF, MeasureTheory.integral_eq_lintegral_pos_part_sub_lintegral_neg_part, MeasureTheory.Integrable.integral_eq_integral_meas_lt, MeasureTheory.integral_nonneg_of_ae, MeasureTheory.integral_add, MeasureTheory.integral_mono, MeasureTheory.integral_eq_zero_iff_of_nonneg_ae, MeasureTheory.integral_congr_ae, MeasureTheory.integral_const, MeasureTheory.norm_integral_le_integral_norm, MeasureTheory.integral_indicator_one, ProbabilityTheory.IndepFun.integral_mul_eq_mul_integral, MeasureTheory.integral_map, MeasureTheory.mul_meas_ge_le_lintegral, ProbabilityTheory.meas_ge_le_variance_div_sq, ConvexOn.map_integral_le, MeasureTheory.eLpNorm_le_eLpNorm_of_exponent_le, ENNReal.lintegral_mul_le_Lp_mul_Lq, integral_inner, MeasureTheory.eLpNorm_add_le, MeasureTheory.lintegral_iSup, MeasureTheory.lintegral_liminf_le, MeasureTheory.tendsto_integral_of_dominated_convergence |
| Q237193 | Exponential distribution | ProbabilityTheory.expMeasure, ProbabilityTheory.exponentialPDFReal, ProbabilityTheory.cdf_expMeasure_eq |
| Q168698 | Exponential function | Real.exp, Real.exp_add, Real.tendsto_exp_div_pow_atTop, Real.exp_pos, Real.hasDerivAt_exp, Real.exp_log, Complex.exp, Complex.isCauSeq_norm_exp, Real.tendsto_one_add_div_pow_exp, Real.exp_neg, Real.exp_strictMono, Real.rpow, analyticOnNhd_cexp, Complex.tendsto_one_add_div_pow_exp, Complex.exp_add, Complex.exp_log, Complex.exp_periodic, Complex.exp_conj, Complex.norm_exp, Complex.exp_mul_I, Complex.exp_eq_exp_re_mul_sin_add_cos, Complex.two_cos, NormedSpace.exp, NormedSpace.isUnit_exp |
| Q582659 | Exponential growth | isLittleO_rpow_exp_atTop |
| Q33456 | Exponentiation | Monoid.npow, pow_add, zpowRec, Real.rpow, sq, pow_zero, zpow_neg, DivInvMonoid.zpow, zpow_add, Commute.add_pow, Fintype.card_fun, Fintype.card_finset, one_pow, zero_pow, neg_one_pow_eq_pow_mod_two, tendsto_pow_atTop_atTop_of_one_lt, tendsto_pow_atTop_nhds_zero_of_lt_one, Real.zero_rpow, Real.rpow_def_of_pos, Real.exp_add, Real.exp, Complex.exp, Complex.cpow_def_of_ne_zero, Complex.exp_mul_I, Complex.norm_mul_exp_arg_mul_I, IsPrimitiveRoot.card_nthRoots, rootsOfUnity, IsPrimitiveRoot, Complex.isPrimitiveRoot_exp, Complex.cpow_def, Complex.log, Complex.cpow, Group, Subgroup.zpowers, orderOf, orderOf_dvd_card, IsNilpotent, nilradical, IsReduced, Ideal.radical, MvPolynomial.vanishingIdeal_zeroLocus_eq_radical, iteratedDeriv, Field, GaloisField, add_pow_char, frobenius, Set.prod, Cardinal.power_def, Equiv.curry, Set.powerset, CategoryTheory.ihom.adjunction, hyperoperation, Function.comp, Nat.iterate, Function.invFun, npowBinRec, Real.tendsto_one_add_div_pow_exp, Complex.arg_mul, orderOf_eq_card_of_zpowers_eq_top, Equiv.sumArrowEquivProdArrow, FiniteField.pow_card, IsPrimitiveRoot.card_primitiveRoots, Ideal.radical_idem |
| Q1196652 | Exterior algebra | ExteriorAlgebra, ExteriorAlgebra.exteriorPower, ExteriorAlgebra.gradedAlgebra, ExteriorAlgebra.lift, ExteriorAlgebra.ιMulti, ExteriorAlgebra.ι_sq_zero, ExteriorAlgebra.ι_add_mul_swap, AlternatingMap.map_perm, Module.Basis.exteriorPower, exteriorPower.finrank_eq, MultilinearMap.alternatization, AlternatingMap, exteriorPower.alternatingMapLinearEquiv, ExteriorAlgebra.map |
| Q120976 | Factorial | Nat.factorial, Nat.factorial_zero, Nat.factorial_succ, Fintype.card_perm, Nat.choose_mul_factorial_mul_factorial, numDerangements, Nat.exists_infinite_primes, Nat.exists_prime_lt_and_le_two_mul, Nat.eventually_pow_lt_factorial_sub, Stirling.tendsto_stirlingSeq_sqrt_pi, Nat.dvd_factorial, Nat.Prime.emultiplicity_factorial, Nat.Prime.emultiplicity_choose, Nat.prime_iff_fac_equiv_neg_one, Nat.factorial_mul_factorial_dvd_factorial_add, Real.Gamma_eq_integral, Complex.Gamma_add_one, Complex.Gamma_mul_Gamma_one_sub, Complex.differentiableAt_Gamma, Real.eq_Gamma_of_log_convex, Complex.digamma, Nat.doubleFactorial, Nat.descFactorial, primorial, Nat.superFactorial, Complex.exp_eq_exp_ℂ, add_pow, HasFTaylorSeriesUpToOn.comp, Real.tendsto_prod_pi_div_two, ascPochhammer, Fintype.card_embedding_eq, ProbabilityTheory.poissonPMFReal |
| Q623950 | Fast Fourier transform | ZMod.dft |
| Q132469 | Fermat's Last Theorem | FermatLastTheorem, FermatLastTheorem.of_odd_primes, fermatLastTheoremFor_iff_int, fermatLastTheoremFor_iff_rat, norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero, PythagoreanTriple, PythagoreanTriple.classification, fermatLastTheoremFour, FermatLastTheoremFor.mono, fermatLastTheoremThree, CyclotomicField, WeierstrassCurve.IsElliptic, ModularForm |
| Q188295 | Fermat's little theorem | Int.ModEq.pow_prime_eq_self, Int.ModEq.pow_card_sub_one_eq_one, Int.prime_dvd_pow_sub_one, Nat.ModEq.pow_totient, lucas_primality, Nat.FermatPsp |
| Q1154996 | Fiber bundle | FiberBundle, Bundle.Trivial.fiberBundle, FiberBundle.mem_baseSet_trivializationAt, Trivialization, FiberBundle.homeomorphAt, FiberBundle.isOpenMap_proj, VectorBundle, TangentBundle, FiberBundleCore.coordChange_comp |
| Q23835349 | Fibonacci sequence | Nat.fib, Nat.fib_add_two, Int.fib, Int.fib_neg_natCast, Real.coe_fib_eq, Real.goldenRatio, tendsto_fib_succ_div_fib_atTop, Real.goldenRatio_mul_fib_succ_add_fib, Nat.fib_two_mul, Nat.fib_two_mul_add_one, Nat.fib_succ_eq_succ_sum, Int.fib_succ_mul_fib_pred_sub_fib_sq, Int.fib_add_sq_sub_fib_mul_fib_add_two_mul, Nat.fib_gcd, Nat.fib_dvd, Nat.fib_succ_eq_sum_choose, Nat.zeckendorfEquiv |
| Q5446431 | Fibred category | CategoryTheory.Functor.Fiber, CategoryTheory.Functor.IsStronglyCartesian, CategoryTheory.Functor.IsPreFibered.pullbackObj, CategoryTheory.Functor.IsStronglyCartesian.isIso_of_base_isIso, CategoryTheory.Functor.IsCartesian.domainUniqueUpToIso, CategoryTheory.BasedCategory, CategoryTheory.BasedCategory.bicategory, CategoryTheory.Functor.IsFibered, CategoryTheory.Pseudofunctor.CoGrothendieck.forget, CategoryTheory.Functor.IsStronglyCocartesian |
| Q190109 | Field (mathematics) | Field, IsField, Rat.instField, Real.instField, Complex.instField, GaloisField, Field.isDomain, DivisionSemiring.toGroupWithZero, isCyclic_of_subgroup_isDomain, CharP, CharP.char_is_prime_or_zero, frobenius, add_pow_char, Subfield, RingHom, RingHom.injective, FiniteField.card', GaloisField.algEquivGaloisFieldOfFintype, CommRing, Ring.isField_iff_isSimpleOrder_ideal, FractionRing, IsFractionRing.toField, LaurentSeries, IsLocalRing.ResidueField, PrincipalIdealRing.isMaximal_of_irreducible, IntermediateField.adjoin, IntermediateField.sup_def, Algebra, Module.finrank, Module.finrank_mul_finrank, IsAlgebraic, Algebra.IsAlgebraic, Algebra.IsAlgebraic.of_finite, IntermediateField.adjoin.finiteDimensional, Transcendental, IsTranscendenceBasis, exists_isTranscendenceBasis, IsAlgClosed, Complex.isAlgClosed, IsAlgClosure, IsAlgClosure.equivOfAlgebraic, IsStrictOrderedRing, Archimedean, ConditionallyCompleteLinearOrderedField, ConditionallyCompleteLinearOrderedField.to_archimedean, ConditionallyCompleteLinearOrderedField.inducedOrderRingIso, Hyperreal, IsTopologicalDivisionRing, Padic, Differential, IsGalois, Field.exists_primitive_element, AlgEquiv, IsGalois.intermediateFieldEquivSubgroup, IsAlgClosed.equivOfTranscendenceBasis, FirstOrder.Language.ElementarilyEquivalent, FirstOrder.Field.ACF_zero_realize_iff_infinite_ACF_prime_realize, FirstOrder.Language.Ultraproduct.sentence_realize, Field.absoluteGaloisGroup, BrauerGroup, div_mul_cancel₀, Module.Basis.ofVectorSpace, AlgebraicGeometry.Scheme.functionField, NumberField, CyclotomicField, Rat.AbsoluteValue.equiv_real_or_padic, DivisionRing, Quaternion, littleWedderburn, CharP.cast_eq_zero, Surreal, Nimber.instField, Field.toNontrivial, Complex.instMul, mul_eq_zero, neg_one_mul, RingEquiv, MeromorphicOn |
| Q577835 | Field extension | Algebra, Complex.instAlgebraOfReal, Subfield, SubfieldClass, DivisionRing.toRatAlgebra, Rat.castHom, charP_of_injective_ringHom, IntermediateField, Module.finrank, FiniteDimensional, Module.finrank_mul_finrank, IntermediateField.adjoin, IntermediateField.FG, Field.exists_primitive_element, IsScalarTower, RingHom.injective, Zsqrtd, NumberField, AdjoinRoot, Polynomial.SplittingField, GaloisField, RatFunc, IsAlgebraic, minpoly.irreducible, IntermediateField.adjoin.finiteDimensional, algebraicClosure, Algebra.IsAlgebraic, Algebra.IsAlgebraic.of_finite, AlgebraicClosure, AlgebraicIndependent, exists_isTranscendenceBasis, IsTranscendenceBasis.lift_cardinalMk_eq, Normal, IntermediateField.normalClosure, Algebra.IsSeparable, IsGalois.intermediateFieldEquivSubgroup, Algebra.IsCentral, Real.nonempty_algEquiv_or, Quaternion, BrauerGroup, IsAzumaya, Algebra.TensorProduct.instAlgebra |
| Q203066 | Finitary relation | Relator.LeftTotal, Relator.LeftUnique, SetRel, Eq, Dvd.dvd, Membership.mem, Set.prod, Fin |
| Q2068418 | Finite difference | fwdDiff, fwdDiff_aux.fwdDiffₗ, hasDerivAt_iff_tendsto_slope, hasDerivAt_iff_tendsto_slope_zero, Polynomial.fwdDiff_iter_degree_eq_factorial, fwdDiff_smul, shift_eq_sum_fwdDiff_iter, PadicInt.hasSum_mahler, fwdDiff_aux.shiftₗ, fwdDiff_const, IncidenceAlgebra.mu, descPochhammer, Nat.add_choose_eq, Nat.choose, taylor_mean_remainder_lagrange, fwdDiff_iter_eq_sum_shift |
| Q603880 | Finite field | Fintype.card, GaloisField, FiniteField.card, FiniteField.ringEquivOfCardEq, FiniteField.pow_card, isCyclic_of_subgroup_isDomain, ZMod, CharP, add_pow_char, FiniteField.pow_card_sub_one_eq_one, PerfectField.ofFinite, GaloisField.card, GaloisField.algEquivGaloisField, Fintype.nonempty_field_iff, IsCyclic.card_orderOf_eq_totient, IsPrimitiveRoot, frobenius, FiniteField.frobenius_pow, FiniteField.orderOf_frobeniusAlgEquivOfAlgebraic, GaloisField.instIsGaloisOfFinite, PerfectRing.ofFiniteOfIsReduced, Irreducible, Polynomial.uniqueFactorizationMonoid, AlgebraicClosure, littleWedderburn, CharP.char_is_prime, FiniteField.pow_card_pow, Algebra.IsAlgebraic.isSeparable_of_perfectField |
| Q1057968 | Finite group | Group, Equiv.Perm, Fintype.card_perm, IsCyclic, rootsOfUnity.isCyclic, IsCyclic.monoidHom_mulEquiv_rootsOfUnity, CommGroup, AddCommGroup.equiv_directSum_zmod_of_finite, Subgroup.card_subgroup_dvd_card, Sylow, Equiv.Perm.subgroupOfMulAction, CompositionSeries.jordan_holder, isCyclic_of_prime_card, IsZGroup.of_squarefree |
| Q4055684 | First-order logic | FirstOrder.Language, FirstOrder.Language.Theory, FirstOrder.Language.Structure, FirstOrder.Language.Term, FirstOrder.Language.Relations, FirstOrder.Language.Functions, FirstOrder.Language.Constants, FirstOrder.Language.BoundedFormula, FirstOrder.Language.BoundedFormula.IsAtomic, FirstOrder.Language.BoundedFormula.freeVarFinset, FirstOrder.Language.Sentence, FirstOrder.Language.BoundedFormula.Realize, FirstOrder.Language.Theory.IsSatisfiable, FirstOrder.Language.Theory.ModelsBoundedFormula, FirstOrder.Language.Theory.Model, FirstOrder.Language.Term.bdEqual, FirstOrder.Language.exists_elementarySubstructure_card_eq, FirstOrder.Language.Theory.isSatisfiable_iff_isFinitelySatisfiable, FirstOrder.Language.Theory.exists_model_card_eq, ExistsUnique, FirstOrder.Language.BoundedFormula.IsPrenex |
| Q1479523 | Five lemma | CategoryTheory.Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono, CategoryTheory.Abelian.epi_of_epi_of_epi_of_mono, CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono |
| Q1426191 | Flat module | Module.Flat, Module.FaithfullyFlat, Module.Flat.iff_rTensor_injective, Module.Flat.iff_lTensor_exact, Module.Flat.iff_forall_isTrivialRelation, Module.Flat.iff_forall_exists_factorization, Module.Flat.of_projective, Module.Flat.isTorsionFree, IsDedekindDomain.flat_iff_torsion_eq_bot, Module.Projective.iff_split, Module.Flat.projective_of_finitePresentation, Module.free_of_flat_of_isLocalRing, Module.Flat.directSum_iff, RingHom.Flat, IsLocalization.flat, Module.flat_of_isLocalized_maximal, AlgebraicGeometry.Flat, Module.FaithfullyFlat.iff_flat_and_rTensor_faithful, Module.FaithfullyFlat.of_flat_of_isLocalHom, Module.FaithfullyFlat.instOfNontrivialOfFree, Module.Flat.of_free |
| Q215193 | Floor and ceiling functions | Int.floor, Int.ceil, Int.floor_intCast, Int.fract, Int.fract_nonneg, Int.floor_eq_iff, Int.le_floor, Int.gc_coe_floor, Int.floor_add_intCast, Int.floor_mono, Int.floor_le_ceil, Int.floor_neg, Int.fract_neg, Int.fract_fract, Int.floor_div_natCast, round, Nat.length_digits, Nat.Prime.emultiplicity_factorial, Irrational.beattySeq_symmDiff_beattySeq_pos |
| Q192161 | Formal language | Language, Language.instZero, Language.instMul, Language.mem_inf, Language.compl_compl, Language.instKStar, Language.reverse, FirstOrder.Language.Theory, FirstOrder.Language.Structure, FirstOrder.Language.Theory.Model |
| Q1003025 | Formal power series | PowerSeries, PowerSeries.invOfUnit, PowerSeries.coeff, PowerSeries.coeff_mul, PowerSeries.WithPiTopology.instTopologicalSpace, PowerSeries.coeff_pow, PowerSeries.isUnit_iff_constantCoeff, PowerSeries.mk_one_mul_one_sub_eq_one, PowerSeries.instIsDiscreteValuationRing, PowerSeries.subst, PowerSeries.HasSubst, PowerSeries.derivative, PowerSeries.derivativeFun_mul, PowerSeries.derivative_subst, Polynomial.coeToPowerSeries.algHom, PowerSeries.instIsNoetherianRing, PowerSeries.exists_isWeierstrassFactorization, PowerSeries.aeval, PowerSeries.coeff_invOfUnit, LaurentSeries, HahnSeries.order, HahnSeries.instMul, LaurentSeries.of_powerSeries_localization, LaurentSeries.derivative, MvPowerSeries, MvPowerSeries.WithPiTopology, MvPowerSeries.isUnit_iff_constantCoeff, MvPowerSeries.subst, MvPowerSeries.aeval_unique, HahnSeries, HahnSeries.instField, inv_unique, PowerSeries.C, LaurentSeries.instIsFractionRing |
| Q976981 | Formula | EuclideanSpace.volume_ball, FirstOrder.Language.BoundedFormula |
| Q184410 | Four color theorem | SimpleGraph.degree, SimpleGraph.nonempty_hom_of_forall_finite_subgraph_hom |
| Q1365258 | Fourier analysis | MeasureTheory.Integrable.fourierInv_fourier_eq, VectorFourier.fourierIntegral, MeasureTheory.Lp.fourierTransformₗᵢ, hasDerivAt_exp, Real.fourier_mul_convolution_eq, Fourier.fourierIntegral, FourierTransformInv.fourierInv, hasSum_fourier_series_of_summable, Real.tsum_eq_tsum_fourier_of_rpow_decay, ZMod.dft, ZMod.invDFT_def |
| Q179467 | Fourier series | fourierCoeff, hasSum_zeta_two, tendsto_integral_exp_smul_cocompact, hasSum_sq_fourierCoeff, fourierBasis, UnitAddTorus.mFourierCoeff, ContinuousMap.subalgebra_topologicalClosure_eq_top_of_separatesPoints, hasSum_fourier_series_L2, hasSum_fourier_series_of_summable, banach_steinhaus |
| Q6520159 | Fourier transform | Fourier.fourierIntegral, MeasureTheory.Integrable.fourierInv_fourier_eq, TemperedDistribution.fourier_delta_zero, MeasureTheory.Integrable, MeasureTheory.Lp, Real.zero_at_infty_fourier, MeasureTheory.Lp.inner_fourier_eq, MeasureTheory.Lp.fourierTransformₗᵢ, Real.fourier_mul_convolution_eq, VectorFourier.fourierIntegral_fderiv, VectorFourier.fourierIntegral, TemperedDistribution.fourier_apply, SchwartzMap.fourierTransformCLM, MeasureTheory.charFun, PontryaginDual, VectorFourier.fourierIntegral_add, fourierIntegral_gaussian, SchwartzMap, MeasureTheory.convolution, MeasureTheory.Measure.haarMeasure, Polynomial.hermite, MeasureTheory.Measure.dirac, fourierCoeff, Real.tsum_eq_tsum_fourier, ZMod.dft, gelfandStarTransform |
| Q81392 | Fractal | dimH, NowhereDifferentiable.exists_uniformContinuous_and_not_differentiableAt, cantorSet |
| Q1412452 | Fractal dimension | dimH |
| Q1149022 | Fubini's theorem | MeasureTheory.integral_prod, MeasureTheory.lintegral_prod, Summable.tsum_prod, MeasureTheory.Measure.prod, MeasureTheory.inducedOuterMeasure, ENNReal.tsum_comm, MeasureTheory.integral_prod_mul, integral_gaussian, hasSum_zeta_two |
| Q11348 | Function (mathematics) | Function.graph, Set.range, PFun, sq, Rel, Set.prod, PFun.Dom, riemannZeta, Nat.Partrec, ComputablePred.halting_problem, Int.mul, Set.pi, Function.update, Polynomial, RatFunc, Function.Bijective, Real.log_injOn_pos, Real.arccos, HasStrictFDerivAt.implicitFunction, Real.exp, HasFPowerSeriesAt, Nat.factorial, isEmptyElim, Function.const, Set.rangeFactorization, Set.inclusion, id, Function.comp, Function.comp_assoc, Function.id_comp, Set.image, Set.preimage, Function.Injective, Function.injective_iff_hasLeftInverse, Function.Surjective, Function.surjective_iff_hasRightInverse, Function.bijective_iff_has_inverse, Set.restrict, Set.liftCover, Function.extend, Pi.instAdd, Real.log, Monotone, StrictMonoOn.orderIso, Real.sin, ContMDiffSection, ContDiffMapSupportedIn, Inv.inv, Set.image_union |
| Q190549 | Functional analysis | NormedSpace, InnerProductSpace, exists_hilbertBasis, MeasureTheory.Lp, lp, NormedSpace.inclusionInDoubleDual, banach_steinhaus, exists_extension_norm_eq, ContinuousLinearMap.isOpenMap, LinearMap.continuous_of_isClosed_graph, IsTopologicalAddGroup, ContinuousLinearMap, CStarRing, HasFDerivAt, BaireSpace, SchauderBasis |
| Q864475 | Functor | CategoryTheory.Functor, CategoryTheory.Category.opposite, CategoryTheory.Functor.op, CategoryTheory.prod, CategoryTheory.Functor.hom, CategoryTheory.Functor.map_isIso, CategoryTheory.Functor.comp, CategoryTheory.Cat, CategoryTheory.SingleObj, CategoryTheory.SingleObj.mapHom, TopCat.Presheaf, CategoryTheory.Functor.const, CategoryTheory.Functor.id, CategoryTheory.Functor.diag, CategoryTheory.Limits.lim, CategoryTheory.Limits.colim, FundamentalGroupoid, Representation, CategoryTheory.MonoidalCategory.tensor, CategoryTheory.forget, MonCat.free, FreeGroup, CategoryTheory.Functor.IsRepresentable, CategoryTheory.Functor.category, CategoryTheory.NatTrans, CategoryTheory.Adjunction |
| Q662830 | Fundamental group | FundamentalGroup, LoopSpace, Path.Homotopy, Path.Homotopic.equivalence, Path.trans, Path.Homotopic.Quotient.trans, CategoryTheory.End.group, Path.Homotopic.trans_assoc, FundamentalGroup.fundamentalGroupMulEquivOfPathConnected, SimplyConnectedSpace.ofContractible, SimplyConnectedSpace, FundamentalGroup.map, FundamentalGroupoid.fundamentalGroupoidFunctor, IsCoveringMap, HomotopyGroup.Pi, FundamentalGroupoid |
| Q192760 | Fundamental theorem of algebra | Complex.exists_root, Complex.isAlgClosed, Polynomial.Splits.natDegree_eq_card_roots, IsAlgClosed.exists_aeval_eq_zero, Polynomial.Splits.eq_prod_roots, Polynomial.rootMultiplicity, Polynomial.tendsto_norm_atTop, Differentiable.apply_eq_apply_of_bounded, Module.End.exists_eigenvalue, Real.nonempty_algEquiv_or, Polynomial.IsRoot.norm_lt_cauchyBound |
| Q670235 | Fundamental theorem of arithmetic | Nat.primeFactorsList_unique, UniqueFactorizationMonoid, Nat.Prime.dvd_mul, Nat.exists_prime_and_dvd, Nat.prod_primeFactorsList, Nat.factorization, Nat.factorization_mul, Nat.multiplicative_factorization, Irreducible, Prime.irreducible, IsDedekindDomain |
| Q1217677 | Fundamental theorem of calculus | Continuous.integral_hasStrictDerivAt, intervalIntegral.integral_deriv_eq_sub', intervalIntegral.integral_eq_sub_of_hasDerivAt, intervalIntegral.integral_hasStrictDerivAt_right, VitaliFamily.ae_tendsto_average_norm_sub, intervalIntegral.integral_eq_sub_of_hasDerivAt_of_le, AbsolutelyContinuousOnInterval.integral_deriv_eq_sub |
| Q92552 | Galois theory | solvableByRad, Polynomial.Gal, IsGalois, Field.absoluteGaloisGroup, IsSolvable, Equiv.Perm.not_isSolvable, MulAction.toPermHom, IsGalois.intermediateFieldEquivSubgroup, IsPurelyInseparable, MvPolynomial.esymm, IsKleinFour, CompositionSeries, IntermediateField, Derivation, alternatingGroup.isSimpleGroup, AlgebraicClosure, Algebra.IsSeparable, num_dvd_of_is_root, FixedPoints.intermediateField, IsPrimitiveRoot, Equiv.Perm, IsSimpleGroup, Algebra, quadratic_eq_zero_iff |
| Q44455 | Game theory | Sion.exists_isSaddlePointOn |
| Q117806 | Gamma distribution | ProbabilityTheory.gammaMeasure, ProbabilityTheory.gammaPDFReal, ProbabilityTheory.expMeasure, Real.Gamma |
| Q190573 | Gamma function | Complex.GammaIntegral, Complex.differentiableAt_Gamma, Complex.differentiable_one_div_Gamma, Complex.GammaIntegral_eq_mellin, Complex.Gamma_add_one, Real.eq_Gamma_of_log_convex, Complex.GammaIntegral_add_one, Complex.Gamma_nat_eq_factorial, Complex.Gamma, Complex.GammaSeq, Complex.Gamma_mul_Gamma_one_sub, Complex.Gamma_mul_Gamma_add_half, Complex.Gamma_conj, Real.Gamma_one_half_eq, Real.deriv_Gamma_nat, Real.Gamma_mul_add_mul_le_rpow_Gamma_mul_rpow_Gamma, Complex.not_differentiableAt_Gamma_neg_nat, Real.exists_isMinOn_Gamma_Ioi, Complex.betaIntegral_eq_Gamma_mul_div, Complex.digamma, riemannZeta_one_sub, Real.integral_rpow_mul_exp_neg_mul_Ioi, Complex.integral_cpow_mul_exp_neg_mul_Ioi, riemannZeta_neg_two_mul_nat_add_one |
| Q2658 | Gaussian elimination | Matrix.det_updateRow_smul, Matrix.PosDef |
| Q524607 | General linear group | Matrix.GeneralLinearGroup, LinearMap.GeneralLinearGroup, Matrix.SpecialLinearGroup, LinearMap.GeneralLinearGroup.generalLinearEquiv, Matrix.GeneralLinearGroup.toLin', Matrix.GeneralLinearGroup.mkOfDetNeZero, Matrix.isUnit_iff_isUnit_det, Matrix.card_GL_field, Matrix.scalar, Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity, Matrix.orthogonalGroup, Matrix.symplecticGroup, Matrix.unitaryGroup, Matrix.ProjGenLinGroup, LinearMap |
| Q621550 | General topology | TopologicalSpace, IsOpen, TopologicalSpace.IsTopologicalBasis, instTopologicalSpaceSubtype, instTopologicalSpaceProd, TopologicalSpace.coinduced, DiscreteTopology, IndiscreteTopology, CofiniteTopology, Real.pseudoMetricSpace, PseudoMetricSpace, PrimeSpectrum.zariskiTopology, sierpinskiSpace, OrderTopology, ContinuousAt, continuous_of_discreteTopology, continuousAt_def, Continuous.tendsto, SeqContinuous, Continuous.seqContinuous, continuous_iff_seqContinuous, continuous_iff_continuousAt, closure, continuous_iff_image_closure_subset_closure_image, Continuous.comp, IsCompact.image, IsConnected.image, IsPathConnected.image, IsLindelof.image, ContinuousOn.isSeparable_image, TopologicalSpace.le_def, continuous_id_iff_le, IsOpenMap, Homeomorph, Continuous.homeoOfEquivCompactToT2, TopologicalSpace.induced, CompactSpace, IsCompact, CompactIccSpace.isCompact_Icc, Metric.isCompact_iff_isClosed_bounded, IsCompact.isClosed, IsCompact.tendsto_subseq, exists_embedding_euclidean_of_compact, ConnectedSpace, isPreconnected_iff_subset_of_disjoint, isPreconnected_Icc, IsPreconnected.image, connectedComponent, connectedComponentSetoid, TotallyDisconnectedSpace, TotallySeparatedSpace, TotallySeparatedSpace.totallyDisconnectedSpace, Path, pathComponent, PathConnectedSpace, PathConnectedSpace.connectedSpace, Pi.topologicalSpace, TopologicalSpace.IsTopologicalBasis.prod, isCompact_pi_infinite, T0Space, T1Space, T2Space, T25Space, RegularSpace, CompletelyRegularSpace, NormalSpace, exists_continuous_zero_one_of_isClosed, CompletelyNormalSpace, PerfectlyNormalSpace, ContinuousMap.exists_restrict_eq, SequentialSpace, FirstCountableTopology, SecondCountableTopology, TopologicalSpace.SeparableSpace, LindelofSpace, SigmaCompactSpace, FirstCountableTopology.frechetUrysohnSpace, TopologicalSpace.SecondCountableTopology.to_firstCountableTopology, IsSigmaCompact.isLindelof, UniformSpace.firstCountableTopology, MetricSpace, Metric.instParacompactSpace, TopologicalSpace.metrizableSpace_of_t3_secondCountable, dense_sInter_of_isOpen, IsOpen.baireSpace, TopologicalSpace.MetrizableSpace |
| Q109744257 | Generalized hypergeometric function | FormalMultilinearSeries, AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq, NormedSpace.exp_eq_tsum, ascPochhammer, Real.Gamma, AnalyticOn, FormalMultilinearSeries.radius, summable_of_ratio_test_tendsto_lt_one, ordinaryHypergeometric, Matrix.specialOrthogonalGroup, MeromorphicOn, RatFunc, LieGroup |
| Q685140 | Generalized Riemann hypothesis | DirichletCharacter, DirichletCharacter.LFunction, DirichletCharacter.LSeriesSummable_of_one_lt_re, DirichletCharacter.IsPrimitive, NumberField.dedekindZeta |
| Q10861254 | Generalized Stokes theorem | intervalIntegral.integral_eq_sub_of_hasDerivAt, MeasureTheory.integral2_divergence_prod_of_hasFDerivAt, MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable |
| Q213488 | Geodesic | Manifold.pathELength, Manifold.riemannianEDist |
| Q2662474 | Geometric group theory | SimpleGraph.mulCayley, PresentedGroup, Int.instAddCommGroup, FreeGroup, Monoid.CoprodI, Equiv.Perm, CoxeterSystem, groupCohomology |
| Q173523 | Geometric progression | tendsto_pow_atTop_nhds_zero_of_norm_lt_one, tendsto_pow_atTop_atTop_of_one_lt, summable_geometric_iff_norm_lt_one, geom_sum_eq, tsum_geometric_of_norm_lt_one, tendsto_pow_atTop_nhds_zero_iff |
| Q1306887 | Geometric series | geom_sum_mul, geom_sum_eq, hasSum_geometric_of_norm_lt_one, summable_geometric_iff_norm_lt_one, formalMultilinearSeries_geometric, formalMultilinearSeries_geometric_radius |
| Q8087 | Geometry | ChartedSpace, IsManifold, InnerProductGeometry.angle, EuclideanGeometry.angle, EuclideanSpace.dist_eq, MetricSpace, MeasureTheory.Measure, Similar, MvPolynomial.vanishingIdeal_zeroLocus_eq_radical, Convex |
| Q485520 | Goldbach's conjecture | schnirelmannDensity, Nat.sum_four_squares |
| Q41690 | Golden ratio | Real.goldenRatio_sq, Real.goldenRatio_irrational, Real.goldenRatio_pow_sub_goldenRatio_pow, Nat.fib_add_two, Real.geom_goldenRatio_isSol_fibRec |
| Q173582 | Gradient | gradient, inner_gradient_left, fderiv, HasGradientAt.fderiv_apply, hasGradientAt_iff_isLittleO |
| Q141488 | Graph (discrete mathematics) | SimpleGraph, SimpleGraph.emptyGraph, SimpleGraph.degree, SimpleGraph.Adj, Graph, Graph.IsLoopAt, SimpleGraph.maxDegree_lt_card_verts, SimpleGraph.adjMatrix, Digraph, Quiver.reverse, Quiver, Digraph.Adj, SimpleGraph.IsRegularOfDegree, SimpleGraph.completeGraph, SimpleGraph.Reachable, SimpleGraph.Connected, SimpleGraph.IsBipartite, completeBipartiteGraph, SimpleGraph.pathGraph, SimpleGraph.cycleGraph, SimpleGraph.IsTree, SimpleGraph.IsAcyclic, SimpleGraph.mulCayley, CategoryTheory.Quiv.forget |
| Q504843 | Graph coloring | SimpleGraph.Coloring, SimpleGraph.Colorable, SimpleGraph.chromaticNumber, SimpleGraph.chromaticNumber_eq_iff_colorable_not_colorable, SimpleGraph.Coloring.colorClass, SimpleGraph.partitionable_iff_colorable, SimpleGraph.chromaticNumber_le_card, SimpleGraph.chromaticNumber_eq_one_iff, SimpleGraph.chromaticNumber_top, SimpleGraph.isBipartite_iff_exists_isBipartiteWith, SimpleGraph.IsClique.card_le_chromaticNumber, SimpleGraph.nonempty_hom_of_forall_finite_subgraph_hom |
| Q182598 | Graph of a function | Set.graphOn, Set.mem_graphOn, Set.image_fst_graphOn |
| Q131476 | Graph theory | SimpleGraph, Digraph, Graph, SimpleGraph.Coloring, SimpleGraph.chromaticNumber, SimpleGraph.IsBipartite, SimpleGraph.isTuranMaximal_iff_nonempty_iso_turanGraph, SimpleGraph.Hom, szemeredi_regularity, SimpleGraph.IsTree, SimpleGraph.Walk.IsPath, SimpleGraph.incMatrix, SimpleGraph.adjMatrix, SimpleGraph.degMatrix, SimpleGraph.lapMatrix, SimpleGraph.mulCayley, SimpleGraph.completeGraph, completeBipartiteGraph, SimpleGraph.degree, SimpleGraph.Subgraph, SimpleGraph.induce, SimpleGraph.IsClique, SimpleGraph.IsIndepSet, SimpleGraph.Walk.IsCycle, SimpleGraph.Subgraph.IsMatching, SimpleGraph.Connected, SimpleGraph.IsAcyclic, SimpleGraph.IsRegularOfDegree |
| Q131752 | Greatest common divisor | GCDMonoid.gcd, Nat.gcd, Int.gcd, EuclideanDomain.gcd_zero_right, gcd_eq_zero_iff, dvd_gcd_iff, Nat.Coprime, Nat.gcd_mul_lcm, Nat.factorization_gcd, Nat.gcd_sub_self_left, EuclideanDomain.gcd_val, EuclideanDomain.gcd_self, Int.gcd_eq_gcd_ab, IsCoprime.dvd_of_dvd_mul_right, Nat.gcd_mul_left, Nat.gcd_add_mul_right_left, Nat.gcd_div, Nat.coprime_div_gcd_div_gcd, gcd_comm, gcd_assoc, Nat.Coprime.gcd_mul, GCDMonoid.gcd_mul_lcm, Nat.totient_gcd_mul_totient_mul, GCDMonoid, UniqueFactorizationMonoid.toGCDMonoid, EuclideanDomain.gcd, span_gcd |
| Q83478 | Group (mathematics) | Group, Int.instAddCommGroup, One, Inv, CommGroup, AddGroup, DihedralGroup, left_inv_eq_right_inv, mul_right_injective, mul_left_injective, Group.ofLeftAxioms, MonoidHom, MulEquiv, Subgroup, Subgroup.closure, Subgroup.Normal, QuotientGroup.leftRel, QuotientGroup.Quotient.group, QuotientGroup.quotientKerEquivOfSurjective, PresentedGroup, Rat.instField, ZMod, ZMod.unitsEquivCoprime, IsCyclic, rootsOfUnity, intCyclicMulEquiv, MulAction, LinearMap.GeneralLinearGroup, Representation, Nat.card, Equiv.Perm, orderOf, Subgroup.card_subgroup_dvd_card, AddCommGroup.equiv_directSum_zmod_of_finite, isCyclic_of_prime_card, IsSimpleGroup, IsTopologicalGroup, LieGroup, Monoid, CategoryTheory.Groupoid, Semigroup, GrpCat, MonoidHom.id, FreeGroup, SimpleGraph.mulCayley, FundamentalGroup, Subgroup.center, commutator, Sylow, CompositionSeries.jordan_holder, Matrix.specialOrthogonalGroup, CategoryTheory.GrpObj |
| Q288465 | Group action | MulAction, Representation, Equiv.Perm.applyMulAction, FaithfulSMul, MulAction.IsPretransitive, AddTorsor, MulAction.IsMultiplyPretransitive, Equiv.Perm.isMultiplyPretransitive, MulAction.IsPreprimitive, ProperlyDiscontinuousSMul, ContinuousSMul, ProperSMul, Representation.IsSemisimpleRepresentation, MulAction.orbit, MulAction.orbitRel, MulAction.pretransitive_iff_subsingleton_quotient, MulAction.orbitRel.Quotient, MulAction.IsInvariantBlock, MulAction.IsFixedBlock.orbit, MulAction.fixedPoints, groupCohomology.H0, MulAction.fixedBy, MulAction.stabilizer, MulAction.stabilizer_smul_eq_stabilizer_map_conj, MulAction.orbitEquivQuotientStabilizer, MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group, Monoid.toMulAction, MulAction.quotient, ConjAct, Units.instMulAction, LinearEquiv.applyDistribMulAction, Action, AlgEquiv.applyMulSemiringAction, Flow, Set.mulAction, CategoryTheory.ActionCategory, MulActionHom, CategoryTheory.actionAsFunctor |
| Q1055807 | Group representation | Action.ρAut, Representation, LinearMap.GeneralLinearGroup, Action.IsContinuous, MonoidHom.ker, Representation.IntertwiningMap, Representation.Equiv, Subrepresentation, Representation.IsIrreducible, Representation.IsSemisimpleRepresentation, MulAction, MulAction.bijective, MulAction.toPermHom, CategoryTheory.SingleObj, Action.functorCategoryEquivalence, Rep, MeasureTheory.Measure.haar, MonoidAlgebra.Submodule.exists_isCompl, IsTopologicalGroup, Equiv.Perm |
| Q1451046 | Gödel numbering | Nat.factorization_prod_pow_eq_self, Primrec.nat_strong_rec |
| Q200787 | Gödel's incompleteness theorems | ComputablePred.halting_problem, FirstOrder.Language.Theory.IsComplete, FirstOrder.Field.ACF_isComplete, Function.cantor_injective, Cardinal.IsInaccessible, Cardinal.continuum |
| Q1162676 | Haar measure | borel, MeasurableMul.measurable_const_mul, MeasureTheory.Measure.IsMulLeftInvariant, MeasureTheory.Measure.IsMulRightInvariant, MeasureTheory.Measure.haarMeasure_unique, MeasureTheory.Measure.IsHaarMeasure, MeasureTheory.measure_ne_zero_iff_nonempty_of_isMulLeftInvariant, instIsAddHaarMeasureVolume, MeasureTheory.Measure.haar.index, MeasureTheory.Measure.inv.instIsMulRightInvariant, MeasureTheory.Measure.modularCharacterFun, MeasureTheory.integral, MeasureTheory.integral_mul_left_eq_self |
| Q866116 | Hahn–Banach theorem | exists_extension_of_le_sublinear, Module.Dual.exists_extension_of_le_seminorm, Module.Dual.extendRCLikeₗ, StrongDual.exists_extension, exists_extension_norm_eq, geometric_hahn_banach_compact_closed, geometric_hahn_banach_open, NormedSpace.inclusionInDoubleDualLi |
| Q876215 | Harmonic analysis | VitaliFamily.ae_tendsto_average_norm_sub |
| Q599027 | Harmonic function | InnerProductSpace.HarmonicAt, AnalyticAt.harmonicAt_re, AnalyticAt.harmonicAt_log_norm, HarmonicAt.analyticAt, InnerProductSpace.HarmonicOnNhd.exists_analyticOnNhd_ball_re_eq, HarmonicOnNhd.circleAverage_eq, InnerProductSpace.bounded_harmonic_on_complex_plane_is_constant |
| Q565186 | Hausdorff dimension | dimH, Real.dimH_segment, Real.dimH_univ_eq_finrank, dimH_def, MeasureTheory.Measure.hausdorffMeasure, dimH_countable, Real.dimH_univ_pi_fin, dimH_iUnion |
| Q326908 | Hausdorff space | SeparatedNhds, T2Space, R1Space, R1Space.t2Space_iff_t0Space, SeparationQuotient.t2Space_iff, t2_iff_isClosed_diagonal, TopologicalSpace.t2Space_of_metrizableSpace, instT1SpaceCofiniteTopology, TopologicalSpace.PseudoMetrizableSpace.regularSpace, Prod.t2Space, T2Space.t1Space, instR0Space, R1Space.quasiSober, IsCompact.isClosed, SeparatedNhds.of_isCompact_isCompact, NormalSpace.of_compactSpace_r1Space, t2Space_iff_of_isOpenQuotientMap, isClosed_eq, Continuous.ext_on, T2Space.r1Space, instRegularSpaceOfWeaklyLocallyCompactSpaceOfR1Space, CompleteSpace, ContinuousMap.instCommCStarAlgebra |
| Q5691670 | Hearing the shape of a drum | Module.finrank, EuclideanSpace.volume_ball |
| Q82828 | Hexadecimal | Nat.digits_add_two_add_one |
| Q1617044 | Heyting algebra | HeytingAlgebra, GeneralizedHeytingAlgebra.toDistribLattice, BooleanAlgebra.toBiheytingAlgebra, bot_himp, inf_compl_self, Heyting.Regular.instBooleanAlgebra, TopologicalSpace.Opens.instFrame, himp_bot, Order.Frame, LinearOrder.toBiheytingAlgebra, himp_eq_top_iff, inf_iSup_eq, Heyting.IsRegular, IsCompl, compl_sup_distrib, compl_sup_compl_le, HeytingHom, HeytingHomClass.toBoundedLatticeHomClass |
| Q190056 | Hilbert space | Inner, InnerProductSpace, FiniteDimensional.complete, Summable.of_norm, EuclideanSpace, Complex.normSq, RCLike.innerProductSpace, inner_conj_symm, inner_add_left, inner_self_eq_zero, inner_add_right, InnerProductSpace.Core.toNormedAddCommGroup, norm_add_le, norm_inner_le_norm, InnerProductSpace.toNormedSpace, Submodule.innerProductSpace, lp, lp.instInnerProductSpace, lp.completeSpace, MeasureTheory.Lp, MeasureTheory.L2.innerProductSpace, MeasureTheory.Lp.instCompleteSpace, TemperedDistribution.MemSobolev, RKHS, IsCoercive.continuousLinearEquivOfBilin, Ergodic, ContinuousLinearMap.tendsto_birkhoffAverage_orthogonalProjection, fourierBasis, Submodule.orthogonalProjection, SchwartzMap.integral_inner_fourier_fourier, Orthonormal, norm_add_sq_real, parallelogram_law_with_norm, InnerProductSpaceable, InnerProductSpace.toUniformConvexSpace, exists_norm_eq_iInf_of_complete_convex, Submodule.orthogonalProjectionFn_inner_eq_zero, Submodule.orthogonal_eq_bot_iff, StrongDual, InnerProductSpace.toDual, ContinuousLinearMap.isOpenMap, ContinuousLinearEquiv.ofBijective, LinearMap.continuous_of_isClosed_graph, geometric_hahn_banach_closed_point, ContinuousLinearMap.opNorm, ContinuousLinearMap.adjoint, ContinuousLinearMap.adjoint_adjoint, instCStarAlgebraContinuousLinearMapComplexIdOfCompleteSpace, IsSelfAdjoint, CFC.sqrt, unitary, IsCompactOperator, LinearPMap, LinearPMap.IsClosable, LinearPMap.adjoint, LinearMap.IsSymmetric, WithLp.instProdInnerProductSpace, IsHilbertSum, HilbertBasis, HilbertBasis.mkOfOrthogonalEqBot, EuclideanSpace.basisFun, Orthonormal.tsum_inner_products_le, HilbertBasis.repr, HilbertBasis.tsum_inner_mul_inner, exists_hilbertBasis, TopologicalSpace.SeparableSpace, Submodule.orthogonal, Submodule.sup_orthogonal_of_hasOrthogonalProjection, Submodule.orthogonal_orthogonal_eq_closure, spectrum, IsSelfAdjoint.mem_spectrum_eq_re, Module.End.eigenspace, banach_steinhaus, fourierCoeff, Submodule.isClosed_orthogonal, Submodule.orthogonal_le, real_inner_comm, real_inner_self_nonneg, norm_eq_sqrt_real_inner |
| Q273167 | Hilbert's problems | MeasureTheory.IsProbabilityMeasure, RiemannHypothesis |
| Q5018842 | History of algebra | left_distrib, mul_comm, mul_self_sub_mul_self, add_sq, Nat.chineseRemainder, Polynomial, sq_add_sq_mul, quadratic_eq_zero_iff, PythagoreanTriple, Pell.IsFundamental.eq_zpow_or_neg_zpow, quadratic_ne_zero_of_discrim_ne_sq, Matrix.det, Complex.exists_root, isSolvable_gal_of_irreducible, IsGalois.intermediateFieldEquivSubgroup |
| Q2393733 | History of geometry | EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two |
| Q3893386 | History of mathematical notation | InnerProductGeometry.norm_add_sq_eq_norm_sq_add_norm_sq', Nat.Prime.dvd_mul, Nat.fib, Matrix.cramer, Field, Cardinal.aleph |
| Q185264 | History of mathematics | InnerProductGeometry.norm_add_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two, Nat.Perfect, quadratic_eq_zero_iff, EuclideanGeometry.Sphere.thales_theorem, irrational_sqrt_two, Nat.exists_infinite_primes, EuclideanGeometry.mul_dist_add_mul_dist_eq_mul_dist_of_cospherical, Nat.choose_succ_succ, add_pow, Nat.fib, Real.sin, Zsqrtd.norm_mul, exists_hasDerivAt_eq_slope, Pell.exists_of_not_isSquare, Real.tendsto_sum_pi_div_four, Real.hasSum_arctan, Real.hasSum_cos, Real.cos_eq_tsum, Complex, Complex.I, Complex.exists_root, legendreSym.quadratic_reciprocity, ChartedSpace, Module, Quaternion, BooleanAlgebra, isSolvable_gal_of_irreducible, ZFSet, Padic, MeasureTheory.IsProbabilityMeasure, MeasureTheory.lintegral, Hyperreal, lucas_lehmer_sufficiency |
| Q5870804 | History of the function concept | Differentiable, Continuous, BooleanRing, Classical.epsilon, Partrec, Nat.Partrec, Turing.TM0.Machine, ComputablePred.halting_problem, ZFSet, ZFSet.sep, ZFSet.pair, Prod |
| Q1622692 | Hodge star operator | exteriorPower.inner_ιMulti_ιMulti, Orientation.volumeForm |
| Q5887297 | Hom functor | CategoryTheory.LocallySmall, CategoryTheory.coyoneda, CategoryTheory.yoneda, CategoryTheory.Functor.hom, CategoryTheory.yonedaEquiv, CategoryTheory.MonoidalClosed.internalHom, CategoryTheory.MonoidalClosed, CategoryTheory.ihom.adjunction, CategoryTheory.ihom, CategoryTheory.Functor.IsRepresentable, CategoryTheory.Profunctor.id, CategoryTheory.Adjunction.rightAdjoint_preservesLimits, CategoryTheory.Projective.projective_iff_preservesEpimorphisms_coyoneda_obj, TensorProduct.lift.equiv |
| Q202906 | Homeomorphism | Homeomorph, IsHomeomorph, Homeomorph.mulLeft, Homeomorph.isOpenMap |
| Q1324364 | Homogeneous space | MulAction, MulAction.IsPretransitive, MulAction.toPermHom, ContinuousSMul, MulAction.orbitEquivQuotientStabilizer, MulAction.QuotientAction, AddTorsor |
| Q579978 | Homological algebra | ChainComplex, HomologicalComplex.d, HomologicalComplex.homology, HomologicalComplex.Acyclic, AlgebraicTopology.singularChainComplexFunctor, CategoryTheory.ShortComplex.Exact, CategoryTheory.ShortComplex.ShortExact, CategoryTheory.Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono, CategoryTheory.ShortComplex.SnakeInput.snake_lemma, CategoryTheory.Abelian, CategoryTheory.Functor.rightDerived, Ext, CategoryTheory.Tor, CategoryTheory.SpectralSequence, AlgebraicTopology.singularHomologyFunctor, HomologicalComplex.Hom, QuasiIso, HomologicalComplex.homologyFunctor, CategoryTheory.ShortComplex.ShortExact.δ |
| Q1144780 | Homology (mathematics) | ChainComplex, HomologicalComplex.cycles, HomologicalComplex.homology, HomologicalComplex.homologyFunctor, AlgebraicTopology.singularHomologyFunctor, HomologicalComplex, HomologicalComplex.d_comp_d, HomologicalComplex.ExactAt, CochainComplex, groupHomology, HomologicalComplex.Hom, HomologicalComplex.eulerChar, HomologicalComplex.homologyEulerChar, HomologicalComplex.HomologySequence.snakeInput, CategoryTheory.ShortComplex.SnakeInput.δ |
| Q215111 | Homomorphism | map_one, MulHom, MonoidHom, RingHom, NonUnitalRingHom, LinearMap, AlgHom, Matrix.scalar, MulEquiv, CategoryTheory.Iso, EquivLike.bijective, MulEquiv.ofBijective, Homeomorph, Monoid.End, Monoid.End.instMonoid, Module.End.instRing, MulAut, LinearMap.GeneralLinearGroup, CategoryTheory.mono_iff_injective, CategoryTheory.Mono, CategoryTheory.SplitMono, CategoryTheory.IsSplitMono.mono, CategoryTheory.ConcreteCategory.mono_of_injective, CategoryTheory.epi_iff_surjective, CategoryTheory.Epi, IsLocalization.epi, CategoryTheory.SplitEpi, CategoryTheory.SplitEpi.epi, Con.ker, Con.quotientKerEquivRange, QuotientGroup.con_ker_eq_conKer, FirstOrder.Language.Hom, SimpleGraph.Hom |
| Q746083 | Homotopy | ContinuousMap.Homotopic, HomotopyGroup, RelCWComplex, ContinuousMap.Homotopy, ContinuousMap.Homotopy.curry, ContinuousMap.Homotopic.equivalence, ContinuousMap.Homotopic.comp, ContinuousMap.Homotopy.affine, ContinuousMap.HomotopyEquiv, ContractibleSpace, Homeomorph.toHomotopyEquiv, RealTopologicalVectorSpace.contractibleSpace, ContinuousMap.Nullhomotopic, contractible_iff_id_nullhomotopic, ContinuousMap.HomotopicRel, FundamentalGroup |
| Q1626416 | Homotopy group | HomotopyGroup.Pi, GenLoop, GenLoop.transAt, HomotopyGroup.commGroup |
| Q1627597 | Hopf algebra | HopfAlgebra, LinearMap.convSemiring, HopfAlgebra.antipode_mul, IsGroupLikeElem, GroupLike.instGroup, CategoryTheory.HopfObj, CategoryTheory.BimonObj |
| Q204034 | Hyperbolic functions | Real.sinh, Real.deriv_sinh, Real.cosh, Real.tanh, Complex.analyticOnNhd_sinh, Real.sinh_eq, Complex.sinh, Complex.cosh, Real.tanh_eq, Complex.sinh_mul_I, Complex.sinh_neg, Complex.cosh_add_sinh, Complex.cosh_sq_sub_sinh_sq, Complex.sinh_add, Real.cosh_le_exp_half_sq, Real.sinh_eq_tsum, Real.cosh_eq_tsum, Complex.sinh_add_cosh, Complex.sinh_periodic, Complex.cosh_two_mul, Real.artanh_eq_half_log, Complex.hasSum_sinh, Complex.hasSum_cosh, Complex.cos_add_sin_I |
| Q209306 | Hyperbolic geometry | UpperHalfPlane.im_pos, UpperHalfPlane.upperHalfPlaneSet, UpperHalfPlane.dist_of_re_eq, UpperHalfPlane.isometry_pos_mul |
| Q837414 | Hypercomplex number | CliffordAlgebra, CliffordAlgebraComplex.equiv, Algebra.TensorProduct.instAlgebra |
| Q731894 | Hölder's inequality | ENNReal.lintegral_mul_le_Lp_mul_Lq, ENNReal.HolderConjugate, essSup, MeasureTheory.integral_mul_norm_le_Lp_mul_Lq, NNReal.inner_le_Lp_mul_Lq, ENNReal.lintegral_prod_norm_pow_le, lp.tsum_mul_le_mul_norm, MeasureTheory.MemLp.mono_exponent, MeasureTheory.eLpNorm_le_eLpNorm_mul_eLpNorm_of_nnnorm, Real.young_inequality, ENNReal.lintegral_Lp_add_le, MeasureTheory.eLpNorm_le_eLpNorm_of_exponent_le, MeasureTheory.MemLp.mul |
| Q321119 | Identity function | id, Function.bijective_id, Function.comp_id, Function.End, CategoryTheory.CategoryStruct.id, LinearMap.id, LinearMap.toMatrix_id, isometry_id, continuous_id |
| Q193796 | Imaginary unit | Complex.I, Complex, Complex.I_sq, Complex.I_re, Polynomial, Complex.equivRealProd, Complex.rotation, CliffordAlgebraComplex.ofComplex, CliffordAlgebraComplex.equiv, GaussianInt, GaussianInt.instCommRing, Complex.exp_mul_I, Complex.sqrt_I, Complex.exp_periodic, Complex.cosh_add_sinh |
| Q464118 | Improper integral | MeasureTheory.intervalIntegral_tendsto_integral_Ioi, integral_Ioi_rpow_of_lt, not_integrableOn_Ioi_rpow, MeasureTheory.integrableOn_Ioi_of_intervalIntegral_norm_bounded, integral_gaussian, MeasureTheory.integrable_indicator_iff, MeasureTheory.SimpleFunc.posPart_sub_negPart |
| Q1279571 | Indian mathematics | EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two, PythagoreanTriple, Nat.choose_succ_succ, Nat.sum_range_choose, Nat.factorial, Real.sin, Real.pi_gt_d4, Real.sin_sq_add_cos_sq, mul_zero, quadratic_eq_zero_iff, sq_add_mul_sq_mul_sq_add_mul_sq, Real.deriv_sin, exists_deriv_eq_zero, Real.pi_gt_d6, mul_self_eq_mul_self_iff, Real.sin_add, Real.hasSum_sin, tsum_geometric_of_lt_one, Real.hasSum_arctan, Real.tendsto_sum_pi_div_four, exists_hasDerivAt_eq_slope |
| Q131222 | Information theory | Real.negMulLog_zero, Real.binEntropy, Real.binEntropy_le_log_two, InformationTheory.klDiv |
| Q214159 | Inner product space | InnerProductSpace, HilbertSpace, Inner, inner_conj_symm, InnerProductSpace.add_left, InnerProductSpace.Core.definite, inner_smul_right, real_inner_comm, RCLike.innerProductSpace, EuclideanSpace, Matrix.toInnerProductSpace, InnerProductSpace.Core.toNormedAddCommGroup, norm_inner_le_norm, InnerProductSpace.ofNorm, inner_eq_sum_norm_sq_div_four, Submodule.IsOrtho, inner_map_polarization, Submodule.orthogonal, norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero, OrthogonalFamily.norm_sum, InnerProductGeometry.angle, re_inner_eq_norm_add_mul_self_sub_norm_sub_mul_self_div_four, InnerProductSpace.rclikeToReal, OrthonormalBasis, HilbertBasis, exists_hilbertBasis, HilbertBasis.repr, fourierBasis, InnerProductSpace.gramSchmidt, Submodule.orthogonalProjectionOnto, ContinuousLinearMap, LinearMap.IsSymmetric, LinearIsometry, IsometryEquiv.toRealAffineIsometryEquiv, LinearIsometryEquiv, LinearMap.IsSymmetric.diagonalization, QuadraticForm.sigPos_of_equiv_weightedSumSquares, IsRiemannianManifold, ExteriorAlgebra.exteriorPower, CliffordAlgebra |
| Q12503 | Integer | Int, Denumerable.int, Int.instCommRing, Int.instAddCommGroup, CommRingCat.zIsInitial, RingHom.injective_int, instIsAddCyclicInt, intCyclicAddEquiv, Int.instCommMonoid, Int.instIsDomain, Int.not_isField, Rat.isFractionRing, Int.ediv_emod_unique'', Int.euclideanDomain, Nat.primeFactorsList_unique, Int.instLinearOrder, Int.instIsStrictOrderedRing, sub_eq_add_neg, Equiv.intEquivNat, Cardinal.mk_int, Function.Bijective |
| Q4846249 | Integer factorization | Nat.primeFactorsList, Nat.primeFactorsList_unique |
| Q80091 | Integral | intervalIntegral, intervalIntegral.integral_eq_sub_of_hasDerivAt, integral_pow, MeasureTheory.Integrable, BoxIntegral.TaggedPrepartition, BoxIntegral.integralSum, BoxIntegral.integral, MeasureTheory.lintegral, MeasureTheory.Measure.haarMeasure, MeasureTheory.integral, intervalIntegral.integral_add, MeasureTheory.integral_add, intervalIntegral.integral_mono, MeasureTheory.setIntegral_mono_set, intervalIntegral.abs_integral_le_integral_abs, ENNReal.lintegral_mul_le_Lp_mul_Lq, ENNReal.lintegral_Lp_add_le, intervalIntegral.integral_symm, intervalIntegral.integral_same, intervalIntegral.integral_add_adjacent_intervals, intervalIntegral.integral_hasDerivAt_right, MeasureTheory.AECover.integral_tendsto_of_countably_generated, MeasureTheory.integral_prod, intervalIntegral.integral_comp_smul_deriv, intervalIntegral.integral_mul_deriv_eq_deriv_mul |
| Q187631 | Interpolation | AffineMap.lineMap, AffineMap.lineMap_apply_ring, Lagrange.interpolate, Lagrange.eq_interpolate_iff |
| Q185148 | Interval (mathematics) | Set.Icc, unitInterval, Set.OrdConnected, Real.instConditionallyCompleteLinearOrder, Set.Ioo, Real.isTopologicalBasis_Ioo_rat, isClosed_Icc, Set.Ico, BddBelow, Real.diam_Icc, interior_Icc, isPreconnected_iff_ordConnected, convex_iff_ordConnected, closure_Ioo, Set.OrdConnected.inter, Real.ball_eq_Ioo, instOrderTopologyReal, Metric.continuous_iff, intermediate_value_Icc, OrderTopology.completelyNormalSpace, BoxIntegral.Box, Set.ordConnectedComponent, Finset.Icc, IsPreconnected.image, EReal, intervalIntegral, Bornology.IsBounded |
| Q16743426 | Introduction to gauge theory | Circle.instCommGroup, CommGroup, Group, Int.instAddCommGroup |
| Q176786 | Intuitionistic logic | Classical.em, not_forall_of_exists_not, and_imp, iff_iff_implies_and_implies, not_and_self_iff, absurd, Or.resolve_left, mt, Classical.byContradiction, peirce, HeytingAlgebra, BooleanAlgebra, not_and_or |
| Q1855669 | Invariant theory | MvPolynomial.esymmAlgHom_fin_bijective |
| Q674533 | Inverse trigonometric functions | Real.arcsin, Real.sin_periodic, Real.cos_arcsin, Real.arccos_eq_pi_div_two_sub_arcsin, Real.arcsin_neg, Real.arctan_inv_of_pos, Real.arctan_add, Real.hasDerivAt_arctan, Real.hasSum_arctan, Complex.arg, Real.arctan_mem_Ioo, Real.tendsto_arctan_atTop, Real.tan_add, Real.sinOrderIso |
| Q9267097 | Inversive geometry | EuclideanGeometry.inversion, EuclideanGeometry.inversion_involutive, EuclideanGeometry.inversion_of_mem_sphere, EuclideanGeometry.image_inversion_sphere_dist_center, EuclideanGeometry.image_inversion_affineSubspace_of_mem, EuclideanGeometry.image_inversion_perpBisector, EuclideanGeometry.Sphere.isTangentAt_orthRadius_iff_mem, stereographic, EuclideanGeometry.dist_inversion_inversion, Complex.inv_def, Isometry, Dilation |
| Q242188 | Invertible matrix | Invertible, Matrix.inv_eq_left_inv, Matrix.inv, Matrix.isUnit_iff_isUnit_det, Matrix.det, Matrix.adjugate, Matrix.inv_def, Matrix.invOf_fromBlocks₂₂_eq, Matrix.fromBlocks, Matrix.add_mul_mul_inv_eq_sub, Matrix.det_one_add_mul_comm, Matrix.transpose_nonsing_inv, LinearMap.ker_eq_bot, Matrix.linearIndependent_cols_iff_isUnit, Matrix.nonsing_inv_apply, mul_eq_one_comm, Matrix.GeneralLinearGroup |
| Q189112 | Isomorphism | CategoryTheory.IsIsomorphic, CategoryTheory.Aut, ZMod.ringEquivOfPrime, QuotientGroup.quotientKerEquivRange, Isometry, Homeomorph, Diffeomorph, Equiv.Perm, Real.log_mul, Real.exp_add, Real.exp_log, ZMod.chineseRemainder, RelIso, OrderIso, LinearEquiv, MulEquiv, RingEquiv, CategoryTheory.Aut.instGroup, SimpleGraph.Iso, LinearIsometryEquiv, CategoryTheory.Iso, CategoryTheory.isIsomorphicSetoid, CategoryTheory.Iso.trans, CategoryTheory.isomorphismClasses, Cardinal.eq, LinearEquiv.ofFinrankEq, Ordinal |
| Q1065966 | Isomorphism theorems | QuotientGroup.quotientKerEquivRange, QuotientGroup.quotientInfEquivProdNormalQuotient, QuotientGroup.quotientQuotientEquivQuotient, QuotientGroup.comapMk'OrderIso, RingHom.quotientKerEquivRange, RingCon.comapQuotientEquivRange, DoubleQuot.quotQuotEquivQuotOfLE, Ideal.relIsoOfSurjective, LinearMap.quotKerEquivRange, LinearMap.quotientInfEquivSupQuotient, Submodule.quotientQuotientEquivQuotient, Submodule.comapMkQRelIso, Submodule.finrank_quotient_add_finrank, SemidirectProduct |
| Q838495 | Jordan normal form | Module.End.genEigenspace, LinearMap.finrank_range_add_finrank_ker, Module.End.maxGenEigenspaceIndex, Module.End.exists_isNilpotent_isSemisimple, spectrum.map_polynomial_aeval_of_degree_pos, Matrix.charpoly_units_conj, LinearMap.aeval_self_charpoly, minpoly, IsCompactOperator.hasEigenvalue_iff_mem_spectrum, Module.End.eigenspace, Matrix.charpoly, IsNilpotent, Module.End.IsSemisimple, Module.equiv_free_prod_directSum, resolvent |
| Q1765138 | Kerala school of astronomy and mathematics | tsum_geometric_of_lt_one, Real.hasSum_sin, Real.hasSum_cos, Real.tendsto_sum_pi_div_four, Real.deriv_sin |
| Q11476 | Kinematics | Isometry, Matrix.mem_orthogonalGroup_iff' |
| Q550593 | Klein four-group | IsKleinFour, IsKleinFour.mul_self, instIsAddKleinFourProdZModOfNatNat, AddCommGroup.equiv_directSum_zmod_of_finite, DihedralGroup.instIsKleinFourOfNatNat, alternatingGroup.kleinFour, IsKleinFour.isMulCommutative, IsKleinFour.eq_mul_of_ne_all, IsKleinFour.card_four, ZMod |
| Q192826 | Kronecker delta | Matrix.one_apply, orthonormal_iff_ite, Matrix.one_apply_eq, MeasureTheory.Measure.dirac, Finset.sum_ite_eq', IncidenceAlgebra.one_apply, PMF.pure_apply |
| Q1225713 | Krull dimension | ringKrullDim, ringKrullDim_eq_zero_of_field, Ring.krullDimLE_zero_and_isLocalRing_tfae, RelSeries.length, Ideal.primeHeight, Ideal.primeHeight_eq_zero_iff, Ideal.sup_primeHeight_of_maximal_eq_ringKrullDim, Ideal.finiteHeight_of_isNoetherianRing, Ideal.height_le_iff_exists_minimalPrimes, Ideal.height, PrimeSpectrum.topologicalKrullDim_eq_ringKrullDim, MvPolynomial.ringKrullDim_of_isNoetherianRing, Polynomial.ringKrullDim_of_isNoetherianRing, IsPrincipalIdealRing.ringKrullDim_eq_one, Ring.KrullDimLE.isField_of_isDomain, ringKrullDim_eq_bot_of_subsingleton, ringKrullDim_nonneg_of_nontrivial, isArtinianRing_iff_isNoetherianRing_krullDimLE_zero, Module.supportDim |
| Q255166 | Kullback–Leibler divergence | InformationTheory.klDiv, InformationTheory.integral_llr_add_sub_measure_univ_nonneg |
| Q190557 | L'Hôpital's rule | HasDerivAt.lhopital_zero_nhds, hasFDerivWithinAt_closure_of_tendsto_fderiv |
| Q598870 | Lagrange multiplier | IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt, IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt_1d |
| Q505798 | Lagrange's theorem (group theory) | Subgroup.card_subgroup_dvd_card, Subgroup.index_mul_card, QuotientGroup.leftRel, Subgroup.relIndex_mul_index, orderOf_dvd_natCard, Nat.ModEq.pow_totient, isCyclic_of_prime_card, exists_prime_orderOf_dvd_card, Sylow.exists_subgroup_card_pow_prime, alternatingGroup.kleinFour, ZMod.pow_card_sub_one_eq_one |
| Q203484 | Laplace operator | Laplacian.laplacian, InnerProductSpace.HarmonicAt, InnerProductSpace.laplacian_eq_iteratedFDeriv_orthonormalBasis, InnerProductSpace.laplacian_eq_iteratedFDeriv_complexPlane, InnerProductSpace.laplacian_eq_iteratedFDeriv_stdOrthonormalBasis, ContDiffAt.laplacian_add, SchwartzMap.laplacian_eq_fourierMultiplierCLM, TemperedDistribution.besselPotential, TemperedDistribution.MemSobolev, InnerProductSpace.laplacianWithin |
| Q199691 | Laplace transform | ProbabilityTheory.mgf |
| Q339444 | Laplace's equation | InnerProductSpace.HarmonicAt, InnerProductSpace.HarmonicOnNhd.add, InnerProductSpace.HarmonicContOnCl.circleAverage_poissonKernel_smul, AnalyticAt.harmonicAt_re, HarmonicAt.analyticAt, HarmonicOnNhd.circleAverage_eq |
| Q1096885 | Lattice (group) | IsZLattice, ZLattice.module_free, ZLattice.module_finite, ZSpan.fundamentalDomain, exists_ne_zero_mem_lattice_of_measure_mul_two_pow_lt_measure, PeriodPair.lattice, ZLattice.rank, Submodule.IsLattice |
| Q595364 | Lattice (order) | Lattice, Set.instBooleanAlgebra, Finset.sup', Lattice.mk', BoundedOrder, Finset.instLattice, Setoid.completeLattice, Nat.instLattice, Prod.instLattice, CompleteLattice.toBoundedOrder, LatticeHom, BoundedLatticeHom, SupHomClass.toOrderHomClass, Sublattice, CompleteLattice, completeLatticeOfCompleteSemilatticeSup, ConditionallyCompleteLattice, DistribLattice, exists_birkhoff_representation, IsModularLattice, Submodule.instIsModularLattice, IsLowerModularLattice, IsCompl, ComplementedLattice, GradeOrder, CovBy, SupIrred, SupPrime, SupPrime.supIrred, IsAtom, IsAtomic |
| Q164321 | Law of cosines | EuclideanGeometry.law_cos, EuclideanGeometry.Sphere.dist_sq_eq_mul_dist_of_tangent_and_secant, EuclideanGeometry.mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_pi, Real.sin_add, Real.sin_sq_add_cos_sq, EuclideanGeometry.law_sin, InnerProductGeometry.norm_sub_sq_eq_norm_sq_add_norm_sq_sub_two_mul_norm_mul_norm_mul_cos_angle, inner_sub_sub_self |
| Q207952 | Law of large numbers | ProbabilityTheory.strong_law_ae |
| Q170181 | Law of sines | EuclideanGeometry.law_sin, EuclideanGeometry.sin_angle_div_dist_eq_sin_angle_div_dist |
| Q102761 | Least common multiple | Int.lcm, GCDMonoid.lcm_zero_right, Finset.lcm, dvd_def, GCDMonoid.lcm, GCDMonoid.gcd_mul_lcm, Nat.primeFactorsList_unique, Nat.factorization_lcm, Associates.instPartialOrder, Associates.instLattice, UniqueFactorizationMonoid.toGCDMonoid, span_singleton_inf_span_singleton |
| Q853831 | Lebesgue integral | MeasureTheory.integral, MeasureTheory.lintegral, MeasureTheory.lintegral_eq_lintegral_meas_lt, MeasureTheory.MeasureSpace, Measurable, Measurable.iSup, MeasureTheory.lintegral_indicator, MeasureTheory.SimpleFunc, MeasureTheory.SimpleFunc.lintegral, MeasureTheory.SimpleFunc.integral, MeasureTheory.SimpleFunc.eapprox, MeasureTheory.integral_eq_lintegral_pos_part_sub_lintegral_neg_part, MeasureTheory.Integrable, integral_re_add_im, MeasureTheory.integrable_norm_iff, Filter.EventuallyEq, MeasureTheory.lintegral_congr_ae, MeasureTheory.integrable_congr, MeasureTheory.integral_add, MeasureTheory.integral_mono, MeasureTheory.lintegral_iSup, MeasureTheory.lintegral_liminf_le, MeasureTheory.tendsto_integral_of_dominated_convergence |
| Q827230 | Lebesgue measure | Real.volume_Icc, MeasureTheory.OuterMeasure.IsCaratheodory, MeasureTheory.OuterMeasure.caratheodory, Real.measureSpace, Real.volume_Ioo, MeasureTheory.NullSingletonClass.measure_singleton, Real.volume_Icc_pi, MeasurableSet.nullMeasurableSet, Set.Countable.measure_zero, MeasureTheory.Measure.addHaar_affineSubspace, EuclideanSpace.volume_ball, measurableSet_Icc, MeasureTheory.measure_iUnion, MeasurableSet.compl, MeasureTheory.measure_mono, MeasurableSet.iUnion, IsOpen.measurableSet, MeasurableSet.exists_isOpen_diff_lt, Real.locallyFinite_volume, MeasureTheory.Measure.IsOpenPosMeasure, MeasureTheory.measure_mono_null, MeasureTheory.measure_preimage_add, MeasureTheory.Measure.addHaar_smul, MeasureTheory.Measure.addHaar_image_linearMap, MeasureTheory.Measure.IsHaarMeasure.sigmaFinite, measure_zero_of_dimH_lt, BoxIntegral.Box, MeasureTheory.OuterMeasure.toMeasure, MeasureTheory.Measure.haarMeasure, MeasureTheory.hausdorffMeasure_pi_real |
| Q664495 | Lie algebra | LieAlgebra, LieRing.ofAssociativeRing, Cross.lieRing, LieRing, lie_skew, leibniz_lie, lie_lie, LieSubalgebra.lieSpan, IsLieAbelian, LieRing.of_associative_ring_bracket, lieEquivMatrix', LieSubalgebra, LieIdeal, LieHom, LieEquiv, LieSubmodule.Quotient.lieQuotientLieAlgebra, LieHom.quotKerEquivRange, LieSubalgebra.normalizer, LieSubalgebra.IsCartanSubalgebra, LieAlgebra.Prod.instLieRing, LieAlgebra.SemiDirectSum, Derivation, Derivation.instLieAlgebra, LieDerivation.inner, LieDerivation.IsKilling.exists_eq_ad, NormedSpace.exp, LieAlgebra.SpecialLinear.sl, LieAlgebra.Orthogonal.so, LieAlgebra.Symplectic.sp, skewAdjointMatricesLieSubalgebra, IsSl2Triple, FreeLieAlgebra, LieModule, LieModule.IsFaithful, LieAlgebra.ad, UniversalEnvelopingAlgebra, LieAlgebra.derivedSeries, LieModule.IsNilpotent, LieAlgebra.isEngelian_of_isNoetherian, LieAlgebra.IsSolvable, LieAlgebra.radical, LieAlgebra.IsSimple, LieAlgebra.IsSemisimple, killingForm, LieAlgebra.HasTrivialRadical.instIsKilling, GradedLieAlgebra, LieModule.lowerCentralSeries, LieAlgebra.ExtendScalars.instLieAlgebra |
| Q622679 | Lie group | LieGroup, Matrix.GeneralLinearGroup, Matrix.specialOrthogonalGroup, Matrix.SpecialLinearGroup, Matrix.unitaryGroup, Matrix.orthogonalGroup, Matrix.specialUnitaryGroup, Matrix.symplecticGroup, GroupLieAlgebra, NormedSpace.exp, LieRing.ofAssociativeRing, Prod.instLieGroup, Circle |
| Q177239 | Limit (mathematics) | Metric.tendsto_atTop, Filter.Tendsto, tendsto_nhds_unique, Filter.tendsto_iff_seq_tendsto, Filter.atBot, BddAbove, EuclideanSpace, tendsto_pi_nhds, TendstoUniformly, TendstoUniformly.continuous, Metric.tendsto_nhds, ArchimedeanClass.stdPart, Hyperreal.stdPart_of_tendsto, omegaLimit, HasSum, hasSum_zeta_two, Summable, FormalMultilinearSeries.radius, ContinuousAt, tendsto_nhds_iff_seq_tendsto, Continuous.tendsto, AccPt, accPt_iff_frequently_nhdsNE, IsClosed.mem_of_tendsto, hasDerivAt_iff_tendsto, Filter.Tendsto.add, Filter.Tendsto.mul, Filter.Tendsto.inv, CauchySeq, Filter.Tendsto.cauchySeq, CauchySeq.tendsto_limUnder, CompleteSpace, tendsto_of_tendsto_of_tendsto_of_le_of_le, summable_of_ratio_test_tendsto_lt_one, Metric.tendsto_nhds_nhds, T2Space, MeasureTheory.Lp, Finset.sum_range_succ |
| Q1076611 | Limit inferior and limit superior | Filter.limsup, Filter.Tendsto.limsup_eq, Filter.limsup_eq, Filter.liminf_eq, Filter.liminf_le_limsup, tendsto_of_liminf_eq_limsup, Filter.frequently_lt_of_lt_limsup, isGreatest_mapClusterPt_limsup, limsup_add_le, le_liminf_add, limsup_mul_le, oscillation, Filter.liminf, Filter.limsup_compl, MeasureTheory.measure_limsup_atTop_eq_zero, omegaLimit, Filter.limsSup, Filter.limsInf, Filter.atTop, instCompleteLinearOrderEReal, EReal.limsup_neg, Filter.iInf_le_liminf |
| Q33540 | Limit of a function | Metric.tendsto_nhds_nhds, Metric.tendsto_nhdsWithin_nhds, Function.rightLim, Function.leftLim, nhdsWithin, Filter.Tendsto, Filter.atTop, Filter.atBot, Polynomial.div_tendsto_atTop_zero_of_degree_lt, Filter.instSProd, tendsto_pi_nhds, TendstoUniformlyOn, EuclideanSpace, PiLp, Filter.Tendsto.comp, Filter.tendsto_iff_seq_tendsto, ContinuousAt, nhdsLE_sup_nhdsGE, Filter.Tendsto.add, Filter.Tendsto.mul, Polynomial.div_tendsto_atTop_leadingCoeff_div_of_degree_eq, HasDerivAt.lhopital_zero_right_on_Ioo, tendsto_nhds_unique, continuousAt_iff_punctured_nhds, Filter.Tendsto.squeeze |
| Q82571 | Linear algebra | Module, AddCommGroup, LinearMap, Module.End, LinearEquiv, Submodule, LinearMap.range, Submodule.span, LinearIndependent, Module.Basis, Module.Basis.extend, mk_eq_mk_of_basis, FiniteDimensional.nonempty_linearEquiv_iff_finrank_eq, FiniteDimensional, Submodule.finrank_le, Submodule.finrank_sup_add_finrank_inf_eq, Module.Basis.equivFun, Module.Basis.repr, LinearMap.toMatrix, Matrix.mul_apply, Matrix.mulVecLin, LinearMap.toMatrixAlgEquiv, Matrix.det, Matrix.isUnit_iff_isUnit_det, Matrix.cramer, LinearMap.det, Module.End.HasEigenvalue, Matrix.charpoly, Matrix.IsHermitian.spectral_theorem, Module.Dual, Module.Basis.dualBasis, Module.Dual.eval, Module.evalEquiv, LinearMap.dualMap, LinearMap.toMatrix_transpose, InnerProductSpace, norm_eq_sqrt_re_inner, norm_inner_le_norm, OrthonormalBasis, InnerProductSpace.gramSchmidtOrthonormalBasis, Matrix.conjTranspose, IsStarNormal, Module.Free, Submodule.basisOfPid, Module.Presentation.tautologicalRelations, NormedSpace |
| Q484637 | Linear equation | AffineMap |
| Q207643 | Linear map | LinearMap, Submodule.map, IsLinearMap, LinearMap.map_add, LinearMap.map_smul, map_sum, LinearMap.map_zero, Module.Dual, LinearMap.lsmul, LinearMap.instZero, LinearMap.id, Matrix.toLin', Polynomial.derivative, LinearMap.toMatrix, LinearMap.smulRight, LinearEquiv, Module.Basis.constr, exists_extension_of_le_sublinear, Matrix.planeConformalMatrix, IsConformalMap, LinearMap.comp, ModuleCat, LinearEquiv.symm, LinearMap.instAdd, LinearMap.instSMul, LinearMap.module, Module.End.instSemiring, LinearMap.GeneralLinearGroup, LinearMap.GeneralLinearGroup.generalLinearEquiv, LinearMap.toMatrixAlgEquiv, Matrix.GeneralLinearGroup, LinearMap.ker, LinearMap.finrank_range_add_finrank_ker, LinearMap.rank, Submodule.hasQuotient, LinearMap.ker_eq_bot, LinearMap.range_eq_top, IsNilpotent, basis_toMatrix_mul_linearMap_toMatrix_mul_basis_toMatrix, ContinuousLinearMap, IsBoundedLinearMap.isLinearMap_and_continuous_iff_isBoundedLinearMap, LinearMap.continuous_of_finiteDimensional, LinearMap.comp_assoc, IsBoundedLinearMap |
| Q202843 | Linear programming | IsMinOn.of_isLocalMin_of_convex_univ, IsMaxOn.of_isLocalMax_of_convex_univ |
| Q10861030 | Linear regression | Inner.inner, Matrix.transpose, dotProduct |
| Q1753188 | Linearity | IsLinearMap, AddMonoidHom.toRatLinearMap, AddMonoidHom.toRealLinearMap, AffineMap |
| Q1755697 | Liouville number | Liouville, liouvilleNumber, liouville_liouvilleNumber, Liouville.irrational, Liouville.transcendental, Liouville.exists_pos_real_of_irrational_root, dense_liouville, volume_setOf_liouville, eventually_residual_liouville |
| Q1142704 | Local ring | IsLocalRing, IsLocalRing.ringJacobson_eq_maximalIdeal, IsLocalRing.of_unique_max_ideal, Field.instIsLocalRing, IsDiscreteValuationRing, MvPowerSeries.instIsLocalRing, IsLocalRing.of_surjective', Localization.AtPrime.isLocalRing, ValuationRing, ValuationRing.isLocalRing, Ideal.adicTopology, Ideal.iInf_pow_eq_bot_of_isLocalRing, IsLocalRing.ResidueField, IsLocalHom, IsLocalRing.maximal_ideal_unique, IsLocalRing.notMem_maximalIdeal, IsLocalRing.ResidueField.field |
| Q1572357 | Locally convex topological vector space | LocallyConvexSpace, nhds_hasBasis_absConvex, Homeomorph.addLeft, Seminorm, Norm, WithSeminorms, SeminormFamily.moduleFilterBasis, WithSeminorms.hasBasis_zero_ball, WithSeminorms.tendsto_nhds, gauge, gaugeSeminorm, LocallyConvexSpace.ofBases, WithSeminorms.separating_iff_T1, Cauchy, mem_closure_iff_nhds, convex_iff_pointwise_add_subset, Convex.starConvex, Convex.add, Convex.interior, Convex.closure_interior_eq_closure_of_nonempty_interior, Convex.openSegment_interior_closure_subset_interior, convexHull, totallyBounded_convexHull, absConvexHull, absConvexHull_eq_convexHull_balancedHull, convexHull_eq_union, NormedSpace.toLocallyConvexSpace, WeakBilin.locallyConvexSpace, SchwartzMap, Seminorm.continuous_from_bounded, WithSeminorms.continuous_iff_continuous_comp, WeakDual.isCompact_polar, exists_extension_norm_eq, Balanced, Absorbent, IsTopologicalAddGroup.leftUniformSpace, IsTopologicalAddGroup, Convex, AbsConvex |
| Q11197 | Logarithm | Real.logb, Real.log, Nat.log2, Real.log_mul, Complex.log, Real.exp_log, Real.rpow_logb, Real.log_neg, Real.logb_self_eq_one, Real.logb_mul, Real.log_div, Real.log_pow, Real.log_div_log, intermediate_value_Icc, Real.tendsto_log_atTop, Real.tendsto_log_nhdsGT_zero, Real.deriv_log, logDeriv, integral_log, Real.log_rpow, harmonic, Real.tendsto_harmonic_sub_log, Transcendental, Complex.hasSum_taylorSeries_log, Real.hasSum_log_sub_log_of_abs_lt_one, Nat.primeCounting, Stirling.tendsto_stirlingSeq_sqrt_pi, Complex.arg, Complex.exp_mul_I, Real.logb_rpow, ProbabilityTheory.strong_law_ae, riemannZeta, Complex.norm_def, Complex.norm_mul_exp_arg_mul_I |
| Q8078 | Logic | em, inf_sup_left |
| Q191081 | Logical conjunction | And, and_true, Bool.and_eq_true, and_iff_not_or_not, And.intro, And.left, not_and_or, and_comm, Nat.land, Set.mem_inter_iff |
| Q1052379 | Logistic function | Real.tendsto_sigmoid_atTop, Real.sigmoid, Real.sigmoid_neg, Real.hasDerivAt_sigmoid, Real.analyticAt_sigmoid, Real.sigmoid_pos |
| Q305936 | Lp space | EuclideanSpace.norm_eq, PiLp.norm_eq_sum, PiLp.norm_eq_ciSup, PiLp.normedAddCommGroup, PiLp.completeSpace, lp, lp.norm_eq_tsum_rpow, lp.norm_eq_ciSup, lp.completeSpace, lp.inner_eq_tsum, MeasureTheory.Lp, Filter.EventuallyEq, MeasureTheory.eLpNormEssSup, MeasureTheory.eLpNorm_add_le, MeasureTheory.Lp.instNormedAddCommGroup, MeasureTheory.Lp.norm_def, MeasureTheory.Lp.instCompleteSpace, MeasureTheory.L2.inner_def, HilbertBasis, ENNReal.lintegral_mul_le_Lp_mul_Lq, MeasureTheory.Lp.simpleFunc.denseRange, exists_continuous_zero_one_of_isClosed, ContinuousMap.toLp_denseRange, BoundedContinuousFunction.toLp_denseRange, MeasureTheory.mul_meas_ge_le_pow_eLpNorm, Hamming.instMetricSpace, inner_eq_sum_norm_sq_div_four, Summable.abs, MeasureTheory.Measure.count, essSup, MeasureTheory.AEEqFun, Finset.sum_mul_sq_le_sq_mul_sq, Real.not_summable_one_div_natCast, Real.summable_one_div_nat_rpow, MeasureTheory.Measure.rnDeriv, MeasureTheory.TendstoInMeasure, MeasureTheory.Integrable, NormedSpace.inclusionInDoubleDual |
| Q1068283 | Löwenheim–Skolem theorem | FirstOrder.Language.exists_elementaryEmbedding_card_eq, FirstOrder.Language.exists_elementarySubstructure_card_eq, FirstOrder.Language.exists_elementaryEmbedding_card_eq_of_ge, FirstOrder.Language, FirstOrder.Language.Theory, FirstOrder.Language.Structure, FirstOrder.Language.ElementarySubstructure, Cardinal.Categorical, FirstOrder.Language.skolem₁ |
| Q2539 | Machine learning | ProbabilityTheory.IsGaussianProcess, ProbabilityTheory.multivariateGaussian, SimpleGraph.IsAcyclic |
| Q192089 | Magic square | doublyStochastic, doublyStochastic_eq_convexHull_permMatrix |
| Q679903 | Magma (algebra) | Mul, MulHom, catalan_two, catalan_three, FreeMagma, FreeMagma.lift, Semigroup, Monoid, Group, CommMagma, CommMonoid, CommGroup, MulOneClass, IsLeftCancelMul, IsRightCancelMul, IsCancelMul, MagmaCat |
| Q186386 | Map projection | ConformalAt, stereographic |
| Q176645 | Markov chain | ProbabilityTheory.IsMarkovKernel, Matrix.mem_rowStochastic_iff_sum, Matrix.IsPrimitive, Ergodic, MeasureTheory.hittingBtwn, ProbabilityTheory.Kernel.IsReversible |
| Q534112 | Martingale (probability theory) | MeasureTheory.Martingale, MeasureTheory.condExp, MeasureTheory.Filtration, MeasureTheory.Adapted, MeasureTheory.MemLp, MeasureTheory.martingale_condExp, MeasureTheory.Submartingale, MeasureTheory.Supermartingale, MeasureTheory.martingale_iff, MeasureTheory.IsStoppingTime, MeasureTheory.submartingale_iff_expected_stoppedValue_mono, MeasureTheory.stoppedProcess, ConvexOn.map_integral_le, ProbabilityTheory.mgf |
| Q7754 | Mathematical analysis | MetricSpace, dist_triangle, dist_comm, dist_nonneg, Stream'.Seq, Filter.Tendsto, ContinuousAt, Continuous, MeasureTheory.Measure, Real.measureSpace, MeasurableSpace, MeasureTheory.Measure.count, Real.volume_Ioo, exists_deriv_eq_zero, CauchySeq, Metric.tendsto_nhds, dense_iInter_of_isOpen, MeasureTheory.integral, InnerProductSpace, NormedSpace, AnalyticOn, MeromorphicOn, VectorFourier.fourierIntegral, fourierCoeff, Function, Classical.choice, IsManifold, Hyperreal, MeasureTheory.measure_iUnion |
| Q186509 | Mathematical constant | Real.sqrt, EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two, IsAlgebraic, Real.pi, integral_gaussian, rootsOfUnity, Real.exp, numDerangements_tendsto_inv_e, Complex.I, Complex.I_sq, Nat.fib, Real.goldenRatio, tendsto_fib_succ_div_fib_atTop, Real.eulerMascheroniConstant, Real.Gamma, riemannZeta, hasSum_zeta_two, Irrational, Transcendental, irrational_sqrt_two, transcendental_liouvilleNumber, Real.ofDigits_const_last_eq_one |
| Q178377 | Mathematical induction | Nat.rec, Nat.le_induction, WellFounded.induction, Finset.sum_range_id, Nat.strong_induction_on, Nat.exists_prime_and_dvd, Real.geom_mean_le_arith_mean_weighted |
| Q1166618 | Mathematical logic | Metric.continuousAt_iff, Cardinal.not_countable_real, Function.cantor_surjective, exists_wellFoundedLT, ZFSet.isOrdinal_notMem_univ, FirstOrder.Language.exists_elementarySubstructure_card_eq, FirstOrder.Language.Theory.isSatisfiable_iff_isFinitelySatisfiable, FirstOrder.Language, ZFSet, Classical.axiomOfChoice, FirstOrder.Language.Theory, ComputablePred.halting_problem |
| Q486902 | Mathematical model | IsLinearMap, MeasureTheory.ProbabilityMeasure, DFA, RegularExpression, Language.kstar_def, Language.IsRegular |
| Q141495 | Mathematical optimization | IsMinOn, IsLocalMin, IsMinOn.of_isLocalMin_of_convex_univ, IsCompact.exists_isMinOn, LowerSemicontinuousOn.exists_isMinOn, IsLocalExtr.hasDerivAt_eq_zero, IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt_1d, IsLocalMax |
| Q156495 | Mathematical physics | intervalIntegral.integral_eq_sub_of_hasDerivAt, IsLocalExtr.deriv_eq_zero, fourierCoeff, IsRiemannianManifold, HilbertSpace, spectrum |
| Q11538 | Mathematical proof | Even.add, Nat.rec, Nat.even_pow, irrational_sqrt_two, Liouville.transcendental, Counterexample.not_irrational_rpow |
| Q395 | Mathematics | FermatLastTheorem, Module, BooleanAlgebra, Function.cantor_surjective, Module.Flat.of_free, Nat.exists_infinite_primes, EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two, ZMod, Real.sin, Group, Field, Ring, SimpleGraph, Matroid, MeasureTheory.Measure, Nat, Int, Rat, Nat.Prime, Real, Complex |
| Q44337 | Matrix (mathematics) | Matrix, Matrix.isUnit_iff_isUnit_det, Matrix.add_apply, Matrix.addCommMonoid, Matrix.smul_apply, Matrix.transpose, Matrix.transpose_add, Matrix.mul_apply, Matrix.mul_assoc, Matrix.hadamard, Matrix.kroneckerMap, Matrix.submatrix, Matrix.toLin', LinearMap.toMatrix_comp, Matrix.rank, LinearMap.finrank_range_add_finrank_ker, Matrix.instRing, Matrix.diagonal, Matrix.one, Matrix.IsHermitian, Matrix.conjTranspose, Matrix.IsHermitian.spectral_theorem, Matrix.PosDef, Matrix.IsHermitian.posDef_iff_eigenvalues_pos, Matrix.toBilin', Matrix.orthogonalGroup, Matrix.specialOrthogonalGroup, Matrix.unitaryGroup, Matrix.trace, Matrix.trace_mul_comm, Matrix.trace_transpose, Matrix.det, Matrix.det_fin_two, Matrix.det_apply, Matrix.det_mul, Matrix.det_succ_row_zero, Matrix.cramer, Module.End.HasEigenvalue, Matrix.charpoly, Matrix.aeval_self_charpoly, Matrix.charpoly_monic, Matrix.adjugate, NormedSpace.exp, Matrix.fromBlocks, LinearMap.toMatrix, Matrix.GeneralLinearGroup, Matrix.SpecialLinearGroup, Matrix.det_isEmpty, Semiring, Matrix.semiring, SimpleGraph.adjMatrix, HasStrictFDerivAt.implicitFunction |
| Q1049914 | Matrix multiplication | Matrix.instHMulOfFintypeOfMulOfAddCommMonoid, Matrix.mul_apply, Matrix.mulVec, Matrix.vecMul, dotProduct, Matrix.vecMulVec, Matrix.toLin_mul, Matrix.toBilin, LinearMap.toMatrix₂, Matrix.center_eq_scalar_image, Matrix.commute_diagonal, Matrix.mul_add, Matrix.smul_mul, Matrix.transpose_mul, Matrix.conjTranspose_mul, Matrix.mul_assoc, Matrix.instRing, Matrix.isUnit_iff_isUnit_det, Matrix.det_mul, Matrix.charpoly_mul_comm, Matrix.semiring, Matrix.diagonal_pow |
| Q1203540 | Maximal ideal | Ideal.IsMaximal, Ideal.Quotient.field, MaximalSpectrum, Ideal.bot_isMaximal, Int.ideal_span_isMaximal_of_prime, PrincipalIdealRing.isMaximal_of_irreducible, MvPolynomial.isMaximal_iff_eq_vanishingIdeal_singleton, Ideal.Quotient.maximal_ideal_iff_isField_quotient, IsLocalRing.ResidueField, isSimpleModule_iff_quot_maximal, Ideal.exists_maximal, Ideal.IsMaximal.isPrime, Ring.KrullDimLE, Ideal.jacobson, Module.Finite.instIsCoatomicSubmodule, PrimeSpectrum, IsSimpleModule, IsSimpleRing, PrimeSpectrum.zariskiTopology, IsLocalRing.jacobson_eq_maximalIdeal, Ideal.exists_le_maximal |
| Q845060 | Maximum and minimum | IsMaxOn, IsLocalMax, IsCompact.exists_isMaxOn, IsLocalExtr.deriv_eq_zero, IsLocalExtr.fderiv_eq_zero, Maximal, IsLUB, IsLeast, IsGreatest, IsLeast.unique, Set.exists_max_image, not_bddAbove_univ, Function.argmin |
| Q1045555 | Maximum likelihood estimation | ProbabilityTheory.multivariateGaussian |
| Q51501 | Maxwell's equations | gradient, hasDerivAt_integral_of_dominated_loc_of_lip |
| Q2796622 | Mean | Finset.centroid, Real.geom_mean_le_arith_mean, Finset.affineCombination, MeasureTheory.average |
| Q189136 | Mean value theorem | exists_hasDerivAt_eq_slope, constant_of_derivWithin_zero, eq_of_derivWithin_eq, IsOpen.exists_eq_add_of_deriv_eq, exists_ratio_hasDerivAt_eq_ratio_slope, domain_mvt, Convex.lipschitzOnWith_of_nnnorm_fderiv_le, IsOpen.is_const_of_fderiv_eq_zero, norm_image_sub_le_of_norm_deriv_le_segment, Convex.norm_image_sub_le_of_norm_fderiv_le, exists_eq_const_mul_intervalIntegral_of_nonneg, exists_hasDerivAt_eq_zero, norm_inner_le_norm, HasDerivAt.lhopital_zero_nhds, intervalIntegral.integral_eq_sub_of_hasDerivAt |
| Q516776 | Measurable function | Measurable, MeasurableSpace.comap, Continuous.measurable, Measurable.add, Measurable.div, Measurable.comp, Measurable.iSup, measurable_of_tendsto_metrizable |
| Q226995 | Median | ConvexOn.map_integral_le |
| Q180953 | Metric space | MetricSpace, dist_self, dist_pos, dist_comm, dist_triangle, hammingDist, HolderWith, Real.metricSpace, EuclideanSpace.dist_eq, WithLp.prod_dist_eq_of_L1, PiLp, MetricSpace.induced, Metric.ball, Metric.mem_nhds_iff, Metric.isOpen_iff, Metric.nhds_basis_ball, TopologicalSpace.MetrizableSpace, Metric.tendsto_atTop, Filter.Tendsto, CauchySeq, Filter.Tendsto.cauchySeq, CompleteSpace, UniformSpace.Completion, Padic, Bornology.IsBounded, Metric.diam, TotallyBounded, TotallyBounded.isBounded, isCompact_iff_totallyBounded_isComplete, CompactIccSpace.isCompact_Icc, lebesgue_number_lemma, Isometry, Isometry.injective, IsometryEquiv, Continuous, SeqContinuous, Metric.continuous_iff, Homeomorph, Metric.uniformContinuous_iff, UniformContinuous.comp_cauchySeq, CompactSpace.uniformContinuous_of_continuous, LipschitzWith, ContractingWith, ContractingWith.exists_fixedPoint, UniformEquiv, dist_eq_norm, kuratowskiEmbedding, NormedSpace, continuous_of_linear_of_bound, IsManifold, MeasureTheory.Measure.hausdorffMeasure, dimH, SimpleGraph.mulCayley, BoundedContinuousFunction, BoundedContinuousFunction.instCompleteSpace, Metric.infDist, Metric.infDist_zero_of_mem_closure, Metric.continuous_infDist_pt, Metric.hausdorffEDist, Metric.NonemptyCompacts.instMetricSpace, GromovHausdorff.GHSpace, Prod.metricSpaceMax, PiCountable.metricSpace, EMetricSpace, PseudoMetricSpace, IsClosed, Metric.tendsto_nhds, Metric.instParacompactSpace, ContinuousLinearMap, Metric.infDist_le_infDist_add_dist, NormedAddCommGroup, UniformContinuous, ContractingWith.fixedPoint_unique, isCompact_iff_isSeqCompact |
| Q757269 | Metric tensor | Bundle.RiemannianMetric, IsRiemannianManifold, Continuous.inner_bundle, Bundle.RiemannianMetric.symm, norm_tangentSpace_vectorSpace, Bundle.RiemannianMetric.inner, Bundle.ContMDiffRiemannianMetric, Bundle.RiemannianMetric.pos, Manifold.IsImmersion, mfderiv, IsContinuousRiemannianBundle, Manifold.pathELength |
| Q464794 | Minkowski space | LinearMap.BilinForm.IsOrtho, LinearMap.BilinForm.toDual, LinearMap.BilinForm.nondegenerate_iff_ker_eq_bot |
| Q1341061 | Minor (linear algebra) | Matrix.det_succ_row, Matrix.inv_def, Matrix.adjugate |
| Q467606 | Model theory | FirstOrder.Language.BoundedFormula, FirstOrder.Language.Sentence, FirstOrder.Language.Theory, FirstOrder.Language.Theory.IsSatisfiable, FirstOrder.Language.Theory.IsComplete, FirstOrder.Language.completeTheory, FirstOrder.Language, FirstOrder.Language.Structure, FirstOrder.Language.Theory.Model, FirstOrder.Language.Substructure, FirstOrder.Language.ElementarySubstructure, FirstOrder.Language.ElementarySubstructure.theory_model_iff, FirstOrder.Language.ElementaryEmbedding, FirstOrder.Language.Embedding.toHom, FirstOrder.Language.LHom.reduct, FirstOrder.Language.Theory.isSatisfiable_iff_isFinitelySatisfiable, FirstOrder.Language.exists_elementarySubstructure_card_eq, FirstOrder.Language.Theory.exists_large_model_of_infinite_model, Set.Definable, FirstOrder.Language.Substructure.isElementary_of_exists, Set.DefinableFun, FirstOrder.Language.Theory.typeOf, FirstOrder.Language.Theory.CompleteType, FirstOrder.Language.DefinableSet.instBooleanAlgebra, FirstOrder.Language.Theory.CompleteType.instCompactSpace, FirstOrder.Language.Ultraproduct.structure, FirstOrder.Language.Ultraproduct.sentence_realize, Cardinal.Categorical, Order.iso_of_countable_dense, FirstOrder.Language.IsFraisseLimit |
| Q319400 | Modular arithmetic | Int.ModEq, Int.ModEq.add, Int.emod, Int.ModEq.trans, Nat.ModEq.pow_totient, Int.ModEq.of_mul_right, Int.ModEq.mul_left_cancel', ZMod.inv, ZMod.instField, ZMod.pow_card, ZMod.wilsons_lemma, ZMod.chineseRemainder, Polynomial.card_roots, IsPrimitiveRoot, ZMod.isCyclic_units_iff, IsSquare, ZMod.euler_criterion, ZMod, Int.emod_lt_of_pos, ZMod.charZero, ZMod.commRing, Int.quotientSpanNatEquivZMod, zmodCyclicMulEquiv, GaloisField.algEquivGaloisField, ZMod.unitsEquivCoprime |
| Q18848 | Module (mathematics) | Module, Module.AEval, AddCommGroup.uniqueIntModule, Module.Free, Pi.module, Submodule, MulOpposite, Module.compHom, Submodule.span, Submodule.instIsModularLattice, LinearMap, LinearEquiv, LinearMap.ker, LinearMap.quotKerEquivRange, ModuleCat.abelian, Module.Finite, Module.Projective, Module.Injective, Module.Flat, IsSimpleModule, IsSemisimpleModule, FaithfulSMul, Module.IsTorsionFree, IsNoetherian, IsArtinian, SetLike.GradedSMul, Representation, Module.toAddMonoidEnd, SheafOfModules |
| Q543956 | Monodromy | IsCoveringMap.liftPath, IsCoveringMap.liftPath_apply_one_eq_of_homotopicRel, IsCoveringMap.fundamentalGroupMulAction, IsCoveringMap.monodromyPerm |
| Q208237 | Monoid | Monoid, Group, Submonoid, Monoid.FG, CommMonoid, Nat.instCommMonoid, PNat.instCancelCommMonoid, SetSemiring, PUnit.commGroup, WithOne, Ring, Matrix.semiring, FreeMonoid, MulOpposite.instMonoid, Prod.instMonoid, Pi.monoid, Function.End, CategoryTheory.End.monoid, List.prod, Monoid.npow, IsUnit, inv_unique, ZPow.zpow, Units.instGroup, IsCancelMul, Algebra.GrothendieckGroup.of_injective, LeftCancelMonoid.groupOfFinite, Algebra.GrothendieckGroup, MulAction, MonoidHom, MonoidHom.mk', MulEquiv, PresentedMonoid, Relation.SymmGen, CategoryTheory.SingleObj, CategoryTheory.SingleObj.category, CategoryTheory.SingleObj.mapHom, MonCat, CategoryTheory.MonObj, IsOrderedMonoid |
| Q232207 | Monte Carlo method | ProbabilityTheory.strong_law_ae |
| Q1948412 | Morphism | CategoryTheory.Category, Quiver.Hom, CategoryTheory.CategoryStruct.comp, CategoryTheory.Category.id_comp, CategoryTheory.Category.assoc, CategoryTheory.ConcreteCategory, CategoryTheory.LocallySmall, CategoryTheory.Mono, CategoryTheory.SplitMono, CategoryTheory.SplitMono.mono, CategoryTheory.Epi, CategoryTheory.SplitEpi, CategoryTheory.SplitEpi.epi, CategoryTheory.SplitMono.splitEpi, ModuleCat.mono_iff_injective, CategoryTheory.Iso, CategoryTheory.IsIso.inv_eq_of_hom_inv_id, CategoryTheory.isIso_of_epi_of_isSplitMono, CategoryTheory.Balanced, CategoryTheory.End, CategoryTheory.Aut, CategoryTheory.Aut.instGroup, GrpCat, TopCat.isoOfHomeo, CategoryTheory.Cat.category, CategoryTheory.Functor.category |
| Q40276 | Multiplication | Nat.nsmul_eq_mul, mul_comm, div_eq_mul_inv, dvd_mul_right, zero_mul, neg_mul_neg, Rat.mul_eq_mkRat, Complex.mul_re, Complex.I_sq, Complex.arg_mul_coe_angle, Finset.prod, Finset.prod_empty, Finset.prod_const, Finset.prod_mul_distrib, tprod, pow_succ, mul_assoc, left_distrib, one_mul, mul_zero, neg_one_mul, inv_mul_cancel, mul_lt_mul_of_pos_left, mul_lt_mul_left_of_neg, Int.instCommRing, Cardinal.mul_def, Group, Rat.instField, Matrix.GeneralLinearGroup, Real, Complex, Ring |
| Q205243 | Möbius function | ArithmeticFunction.moebius, ArithmeticFunction.LSeries_zeta_mul_Lseries_moebius, ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq, ArithmeticFunction.isMultiplicative_moebius, ArithmeticFunction.moebius_mul_coe_zeta, ArithmeticFunction.IsMultiplicative.mul, ArithmeticFunction.moebius_ne_zero_iff_squarefree, ArithmeticFunction.moebius_apply_prime, IncidenceAlgebra.mu |
| Q595742 | Möbius transformation | OnePoint.instGLAction, OnePoint.smul_some_eq_ite, OnePoint.smul_infty_eq_ite, Matrix.GeneralLinearGroup.fixpointPolynomial, OnePoint.equivProjectivization, Matrix.IsParabolic, Matrix.GeneralLinearGroup.IsParabolic.smul_eq_self_iff, Matrix.IsElliptic, Matrix.IsHyperbolic |
| Q903783 | Naive set theory | Set, Set.Mem, Set.ext, Set.instEmptyCollection, Set.eq_empty_of_forall_notMem, Set.instSingletonSet, setOf, Set.Subset, Set.instHasSSubsetSet, Set.instHasSubsetSet, Set.Subset.antisymm, Set.empty_subset, Set.powerset, Set.ncard_powerset, Set.univ, Set.compl, Set.union, Set.inter, Set.diff, Set.instBooleanAlgebra, Prod, Prod.mk.injEq, Set.prod, Nat, Int, Rat, Real, Complex, ZFSet.sep, ZFSet.regularity, ZFSet.mem_irrefl |
| Q204037 | Natural logarithm | Real.log, Real.exp_log, integral_one_div_of_pos, Real.log_mul, Real.log_div_log, Real.log_exp, integral_inv, Real.tendsto_log_nhdsGT_zero, Real.hasSum_pow_div_log_of_abs_lt_one, Real.tendsto_harmonic_sub_log, Real.hasSum_log_one_add_inv, Real.hasDerivAt_log, integral_inv_of_neg, integral_log, Real.artanh_eq_half_log, Complex.log, Complex.log_I |
| Q21199 | Natural number | Nat, Cardinal, Ordinal, Cardinal.mk, Cardinal.eq, Equiv, Cardinal.le_def, Stream'.Seq, IsWellOrder, Ordinal.type, Ordinal.type_nat_lt, PNat, Nat.digits, Nat.succ, Nat.zero, Nat.succ_injective, Nat.succ_ne_zero, Nat.recAux, PSet.ofNat, PSet.omega, Nat.card, Nat.add, Nat.add_succ, Nat.instAddCommMonoid, Nat.instAddCancelCommMonoid, Nat.mul, Nat.factorizationEquiv, Nat.factorization_prod_pow_eq_self, Nat.left_distrib, Nat.instCommSemiring, Nat.instLinearOrder, le_iff_exists_add, Nat.instIsStrictOrderedRing, Nat.find, Nat.div_add_mod, Nat.div, Nat.div_mod_unique, Nat.gcd, Nat.add_assoc, Nat.add_comm, Nat.add_zero, Nat.mul_eq_zero, Int, Rat, Real, Complex |
| Q200227 | Negative number | SignType.sign, lt_trichotomy, Nat, Real.linearOrder, neg_lt_neg_iff, sub_neg_of_lt, Neg, neg_neg_of_pos, Left.add_neg, sub_eq_add_neg, sub_neg_eq_add, mul_neg_of_pos_of_neg, neg_mul_neg, mul_pos_iff, div_pos_of_neg_of_neg, div_pos_iff, add_neg_cancel, neg_add_cancel, neg_neg, abs, Int.instCommRing, Int.instLinearOrder, Algebra.GrothendieckAddGroup, neg_eq_of_add_eq_zero_left, add_left_cancel |
| Q374195 | Newton's method | hensels_lemma, fderiv, intermediate_value_Icc, exists_hasDerivAt_eq_slope |
| Q190529 | Nicolas Bourbaki | one_add_one_eq_two, Set.empty_def, Function.Bijective, Metric.ball |
| Q1755242 | Nilpotent group | Group.IsNilpotent, nilpotent_iff_finite_ascending_central_series, Group.nilpotencyClass, Subgroup.lowerCentralSeries_length_eq_nilpotencyClass, Group.nilpotencyClass_zero_iff_subsingleton, CommGroup.isNilpotent, Group.isNilpotent_prod, IsPGroup.isNilpotent, Group.isNilpotent_of_finite_tfae, IsNilpotent.to_isSolvable, Subgroup.isNilpotent |
| Q233858 | Non-Euclidean geometry | Complex.normSq, Circle, DualNumber, instInvolutiveNegElemSphereOfNat, Projectivization |
| Q617295 | Nondeterministic finite automaton | DFA, NFA, DFA.toNFA_correct, NFA.toDFA_correct, NFA.accepts, NFA.accepts_iff_exists_path, NFA.evalFrom, DFA.toNFA, εNFA, εNFA.εClosure, εNFA.evalFrom, εNFA.accepts, εNFA.toNFA_correct, εNFA.toNFA_evalFrom_match, Language.IsRegular.add, Language.IsRegular.inf, Language.IsRegular.compl |
| Q769909 | Nonlinear programming | IsMinOn.bddBelow |
| Q956437 | Norm (mathematics) | Norm, Seminorm, NormedSpace, SeminormedAddCommGroup, NormedAddCommGroup, norm_nonneg, Norm.norm, Real.norm_eq_abs, EuclideanSpace.norm_eq, inner_self_eq_norm_mul_norm, Complex.isAbsoluteValueNorm, Quaternion.normSq, inner_self_eq_norm_sq, PiLp.norm_eq_of_L1, PiLp.norm_eq_sum, PiLp.norm_eq_ciSup, lp, InnerProductSpace.Core.toNormedAddCommGroup, gaugeSeminorm, Algebra.norm, abs_norm_sub_norm_le, NNReal.inner_le_Lp_mul_Lq, norm_inner_le_norm, convexOn_norm, tendsto_iff_norm_sub_tendsto_zero, ContinuousLinearEquiv.ofFinrankEq |
| Q133871 | Normal distribution | ProbabilityTheory.gaussianReal, ProbabilityTheory.tendstoInDistribution_inv_sqrt_mul_sum_sub, ProbabilityTheory.gaussianReal_const_mul, ProbabilityTheory.gaussianReal_div_const, fourierIntegral_gaussian, ProbabilityTheory.charFun_gaussianReal, ProbabilityTheory.mgf_gaussianReal, ProbabilityTheory.cgf_gaussianReal, ProbabilityTheory.gaussianReal_zero_var, ProbabilityTheory.HasGaussianLaw.indepFun_of_covariance_eq_zero, ProbabilityTheory.gaussianReal_map_linearMap, ProbabilityTheory.gaussianReal_add_gaussianReal_of_indepFun, ProbabilityTheory.multivariateGaussian, ProbabilityTheory.IsGaussianProcess, ProbabilityTheory.IsGaussian, ProbabilityTheory.gaussianPDFReal |
| Q215206 | NP-completeness | ComputablePred.halting_problem |
| Q11563 | Number | Transcendental, Algebraic.countable, irrational_pi, GenContFract.terminates_iff_rat, irrational_sqrt_two, Complex.cos_add_sin_mul_I_pow, Complex.cos_add_sin_I, Complex.exp_pi_mul_I, Complex.exists_root, GaussianInt, CyclotomicField, Nat.Prime, Nat.exists_infinite_primes, Nat.gcd, Nat.prime_iff_fac_equiv_neg_one, not_summable_one_div_on_primes, RiemannHypothesis, Nat, Nat.digits, Nat.succ, Int.negSucc, Int, Int.instCommRing, Rat, Irrational, Real.instConditionallyCompleteLinearOrder, ConditionallyCompleteLinearOrderedField.inducedOrderRingIso, Complex.I, Complex, Complex.re, Complex.isAlgClosed, Even, odd_iff_exists_bit1, Even.mul_right, mersenne, Nat.instUniqueFactorizationMonoid, bernoulli, Nat.fib, Nat.Perfect, IsAlgebraic, IsIntegral, Padic, Quaternion, Ordinal, Cardinal, Hyperreal |
| Q12479 | Number theory | Int, PythagoreanTriple, Mul, Dvd.dvd, Nat.div_add_mod, Nat.three_dvd_iff, Nat.gcd, Nat.Coprime, EuclideanDomain.gcd, GenContFract, Nat.Prime, Nat.exists_infinite_primes, Nat.factorization, Nat.primeFactorsList, Nat.Prime.dvd_mul, Nat.primeFactorsList_unique, ZMod, Int.ModEq, ZMod.pow_card, Nat.ModEq.pow_totient, Filter.Tendsto, Complex.I, Complex.re, Nat.primeCounting, riemannZeta, riemannZeta_eulerProduct, RiemannHypothesis, Ideal.IsPrime, NumberField.dedekindZeta, IsAlgebraic, NumberField, IsAbelianGalois, Real.infinite_rat_abs_sub_lt_one_div_den_sq_of_irrational, Transcendental, ZMod.chineseRemainder, Pell.exists_of_not_isSquare, Nat.prime_iff_fac_equiv_neg_one, Nat.sum_four_squares, legendreSym.quadratic_reciprocity, Nat.infinite_setOf_prime_and_eq_mod, Nat.totient, Nat.Perfect, Nat.divisors |
| Q11216 | Numerical analysis | Lagrange.interpolate, IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt |
| Q82990 | Numerical digit | Nat.ofDigits, Nat.ofDigits_eq_sum_mapIdx |
| Q753445 | Numerical integration | trapezoidal_integral, MeasureTheory.integral_prod |
| Q541182 | Numerical methods for ordinary differential equations | IsPicardLindelof.exists_eq_forall_mem_Icc_hasDerivWithinAt |
| Q728415 | On-Line Encyclopedia of Integer Sequences | ArithmeticFunction.IsMultiplicative, Nat.choose |
| Q213363 | Open set | Metric.isOpen_iff, TopologicalSpace, PseudoMetricSpace.toUniformSpace, isOpen_sUnion, IsClosed, instTopologicalSpaceSubtype, interior, Continuous, IsClopen, isClopen_empty, isOpen_Ioo, BaireMeasurableSet |
| Q131030 | Operator (mathematics) | Module.End, LinearMap, LinearMap.toMatrix, lp, ContinuousLinearMap.toNormedRing, ContinuousLinearMap, ContinuousLinearMap.addCommGroup, gradient, LinearMap.GeneralLinearGroup, Matrix.orthogonalGroup, Matrix.specialOrthogonalGroup, VectorFourier.fourierIntegral |
| Q191780 | Ordinal number | Ordinal, InitialSeg.total, IsWellOrder, Ordinal.type, Ordinal.omega0, Ordinal.lt_wf, OrderIso, Ordinal.isEquivalent, ZFSet.omega, ZFSet.IsOrdinal, ZFSet.IsOrdinal.mem, ZFSet.IsOrdinal.subset_iff_eq_or_mem, Ordinal.bddAbove_of_small, Order.lt_succ, not_small_ordinal, Ordinal.type_eq, Ordinal.zero_or_succ_or_isSuccLimit, Ordinal.bot_eq_zero, Order.succ, Order.IsSuccLimit, Ordinal.isSuccLimit_iff, Order.IsSuccPrelimit.sSup_Iio, Ordinal.omega0_le_of_isSuccLimit, Ordinal.le_iSup, Order.IsNormal, Ordinal.induction, Ordinal.limitRecOn, Ordinal.instPow, Ordinal.not_bddAbove_fp, Ordinal.enumOrd, Ordinal.isPrincipal_add_iff_add_lt_ne_self, Ordinal.epsilon, Ordinal.CNF, Cardinal.ord, Cardinal.isSuccLimit_ord, Ordinal.omega, Ordinal.cof, Ordinal.cof_eq_aleph0_of_isSuccLimit, Ordinal.cof_succ, Ordinal.cof_ord_cof, IsCofinal, Ordinal.IsAcc, Ordinal.isClosed_iff_iSup, Ordinal.epsilon_zero_eq_nfp, derivedSet, exists_wellOrder, Perfect.exists_nat_bool_injection, exists_countable_union_perfect_of_isClosed |
| Q465274 | Ordinary differential equation | IsIntegralCurveOn, IsPicardLindelof.exists_eq_forall_mem_Icc_hasDerivWithinAt |
| Q1783179 | Orthogonal group | Matrix.orthogonalGroup, Matrix.specialOrthogonalGroup, Matrix.mem_orthogonalGroup_iff, LinearIsometryEquiv.instGroup, AffineIsometryEquiv.instGroup, Matrix.det_of_mem_unitary, Matrix.mem_specialOrthogonalGroup_iff, Submodule.reflection, QuadraticForm.equivalent_one_zero_neg_one_weighted_sum_squared, QuadraticForm.equivalent_of_isAlgClosed, char_dvd_card_solutions_of_sum_lt, LieAlgebra.Orthogonal.so, LinearIsometry.isConformalMap, pinGroup, spinGroup |
| Q333871 | Orthogonal matrix | Matrix.orthogonalGroup, Matrix.mem_orthogonalGroup_iff, Matrix.specialOrthogonalGroup, Matrix.permMatrix_one, Equiv.swap, Matrix.det_of_mem_unitary, Matrix.det_permutation, LieAlgebra.Orthogonal.so, NormedSpace.exp_mem_unitary_of_mem_skewAdjoint, Matrix.IsHermitian.spectral_theorem |
| Q215067 | Orthogonality | LinearMap.BilinForm.IsOrtho, Orthonormal, LinearMap.IsSymmetric.orthogonalFamily_eigenspaces |
| Q1268589 | Outer product | Matrix.vecMulVec, Matrix.vecMulVec_eq, Matrix.conjTranspose_vecMulVec, Matrix.trace_vecMulVec, Matrix.vecMulVec_mulVec, vecMulVecBilin, Matrix.rank_vecMulVec_le, TensorProduct.tmul, InnerProductSpace.rankOne, Matrix.det_vecMulVec |
| Q746242 | P versus NP problem | ComputablePred.halting_problem |
| Q311627 | P-adic number | PadicInt, padicNorm, Padic, PadicInt.instCommRing, PadicInt.isUnit_iff, Padic.valuation, padicValRat, padicNormE, PadicInt.instIsDiscreteValuationRing, PadicInt.isUnit_den, PadicInt.instIsDomain, PadicInt.ideal_eq_span_pow_p, Padic.norm_eq_zpow_neg_valuation, Padic.nonarchimedean, Padic.instIsUltrametricDist, PadicInt.compactSpace, PadicInt.ker_toZModPow, Padic.instCharZero, PadicComplex.isAlgClosed, PadicInt.hasSum_mahler, IsDedekindDomain.HeightOneSpectrum.adicCompletion, hensels_lemma, PadicComplex, Padic.adicCompletionEquiv, Padic.add_eq_max_of_ne, PadicInt.toZModPow, Complex.isAlgClosed |
| Q48297 | Parabola | AffineMap |
| Q1413083 | Parameter | Real.logb, Nat.descFactorial, circleMap, ProbabilityTheory.poissonPMF, ProbabilityTheory.gaussianReal |
| Q837683 | Pareto distribution | ProbabilityTheory.paretoPDFReal |
| Q230967 | Parity (mathematics) | Even, Even.zero, even_add_one, even_iff_two_dvd, Odd.add_odd, Odd.mul, Nat.Prime.even_iff, Equiv.Perm.sign, Function.Even, Even.add, Odd, Int.even_iff |
| Q271977 | Partial differential equation | InnerProductSpace.HarmonicAt, InnerProductSpace.instLaplacian |
| Q1756942 | Partial function | PFun, PFun.Dom, Nat.Partrec, partialFunEquivPointed, OpenPartialHomeomorph.trans |
| Q381060 | Partition of a set | Setoid.IsPartition, Setoid.Partition.orderIso, Setoid, Set.PairwiseDisjoint.isPartition_of_exists_of_ne_empty, Finpartition.indiscrete, Setoid.isPartition_classes, Finpartition.instLE, Setoid.Partition.completeLattice, Setoid.completeLattice |
| Q182186 | Pentagram | Real.goldenRatio, DihedralGroup |
| Q1187620 | Perfect graph | SimpleGraph.IsClique, SimpleGraph.cliqueNum, SimpleGraph.Coloring, SimpleGraph.chromaticNumber, SimpleGraph.cliqueNum_le_chromaticNumber, PartialOrder, IncompRel, IsChain, IsAntichain |
| Q170043 | Perfect number | Nat.Perfect, ArithmeticFunction.sigma, Nat.perfect_iff_sum_divisors_eq_two_mul, Theorems100.Nat.perfect_two_pow_mul_mersenne_of_prime, Nat.Prime.of_mersenne, Theorems100.Nat.even_and_perfect_iff, Nat.Abundant, Nat.perfect_iff_sum_properDivisors, Nat.Pseudoperfect, Nat.Weird |
| Q184743 | Periodic function | Function.Periodic, Function.Periodic.int_mul, Int.fract_periodic, Real.sin_periodic, Complex.exp_periodic, Complex.exp_mul_I, Function.Periodic.not_injective, Function.Periodic.intervalIntegral_add_eq, Function.Periodic.const_mul, Function.Periodic.add, Function.Antiperiodic, Real.sin_antiperiodic, Function.Antiperiodic.periodic, Function.Periodic.lift, PeriodPair.weierstrassP_add_coe |
| Q161519 | Permutation | Fintype.card_perm, Equiv.Perm, Equiv.Perm.permGroup, Equiv.Perm.one_def, Equiv.Perm.cycleFactorsFinset_noncommProd, Equiv.Perm.IsCycle, Function.IsFixedPt, derangements, Equiv.swap, Equiv.Perm.Disjoint.commute, Cycle.formPerm_reverse, Equiv.Perm.mul_apply, Equiv.trans, Equiv.trans_assoc, Equiv.symm, Fintype.card_embedding_eq, descPochhammer, Finset.powersetCard, Finset.card_powersetCard, Nat.choose, Fintype.card_pi_const, Equiv.Perm.cycleType, Equiv.Perm.sum_cycleType, Equiv.Perm.card_of_cycleType, IsConj, Equiv.Perm.cycleType_conj, Equiv.Perm.isConj_iff_cycleType_eq, orderOf, Equiv.Perm.lcm_cycleType, Equiv.Perm.truncSwapFactors, Equiv.Perm.sign, Equiv.Perm.sign_mul, Matrix.det_permutation, Equiv.Perm.permMatrix, Matrix.permMatrixHom |
| Q911364 | Perturbation theory (quantum mechanics) | InnerProductSpace, LinearMap.IsSymmetric, HasFPowerSeriesAt, VectorBundle, HilbertBasis, Module.End.HasEigenvalue, HasFDerivAt.comp, IsManifold, unitary, Submodule.orthogonal, Module.End.eigenspace, Matrix.IsDiag, LinearMap.toMatrix |
| Q167 | Pi | Real.pi, irrational_pi, polarCoord, Complex.exp_mul_I, Complex.exp_pi_mul_I, Complex.isPrimitiveRoot_exp, Real.tendsto_prod_pi_div_two, Real.tendsto_sum_pi_div_four, hasSum_zeta_two, BuffonsNeedle.buffon_short, EuclideanSpace.volume_ball_fin_two, EuclideanSpace.volume_ball_fin_three, integral_sqrt_one_sub_sq, Real.sin_periodic, Fourier.fourierIntegral, ProbabilityTheory.gaussianPDFReal, integral_gaussian, fourier_gaussian_pi, Complex.two_pi_I_inv_smul_circleIntegral_sub_inv_smul_of_differentiable_on_off_countable, Real.Gamma_one_half_eq, EuclideanSpace.volume_ball, Stirling.tendsto_stirlingSeq_sqrt_pi, completedRiemannZeta_one_sub, jacobiTheta, jacobiTheta_S_smul, ProbabilityTheory.cauchyPDFReal, Real.pi_lt_d6 |
| Q530152 | Picard–Lindelöf theorem | IsPicardLindelof.exists_eq_forall_mem_Icc_hasDerivWithinAt, ODE.picard_eq_of_hasDerivAt, ODE.picard, ContractingWith.tendsto_iterate_fixedPoint, ContractingWith.exists_fixedPoint, ODE.FunSpace.exists_contractingWith_iterate_next, ODE.FunSpace.dist_iterate_next_apply_le, ContractingWith.isFixedPt_fixedPoint_iterate, ContDiffAt.exists_forall_mem_closedBall_exists_eq_forall_mem_Ioo_hasDerivAt |
| Q188276 | Pigeonhole principle | Fintype.exists_ne_map_eq_of_card_lt, Fintype.exists_lt_card_fiber_of_mul_lt_card, Function.Embedding.isEmpty_of_card_lt, AddCircle.denseRange_zsmul_coe_iff, Finite.exists_ne_map_eq_of_infinite, Fintype.exists_card_fiber_le_of_card_le_mul, Finset.exists_ne_map_eq_of_card_lt_of_maps_to, Fintype.card_le_of_injective, Fintype.card_le_of_surjective, Fintype.exists_le_card_fiber_of_mul_le_card, Fintype.exists_card_fiber_lt_of_card_lt_mul, Cardinal.le_def, Cardinal.exists_uncountable_fiber, Cardinal.infinite_pigeonhole |
| Q44946 | Point (geometry) | Set, EuclideanSpace, AffineSubspace, Module.rank, rank_subsingleton', dimH, dimH_singleton, MeasureTheory.Measure.dirac |
| Q205692 | Poisson distribution | ProbabilityTheory.poissonMeasure, ProbabilityTheory.poissonMeasure_singleton, ProbabilityTheory.tendsto_choose_mul_pow_of_tendsto_mul_atTop |
| Q37555 | Polygon | Polygon, Polygon.edgeSet, Polygon.vertices, Finset.centroid |
| Q43260 | Polynomial | Polynomial, Polynomial.X, Polynomial.eval, Polynomial.comp_X, Polynomial.as_sum_range, Polynomial.leadingCoeff, Polynomial.as_sum_support, Polynomial.degree, Polynomial.C, MvPolynomial.IsHomogeneous, MvPolynomial, Polynomial.coeff_add, Polynomial.coeff_mul, Polynomial.comp, RatFunc, Polynomial.modByMonic_add_div, Polynomial.modByMonic_X_sub_C_eq_C_eval, Polynomial.uniqueFactorizationMonoid, Polynomial.derivative, Polynomial.continuous, Polynomial.tendsto_norm_atTop, isSolvable_gal_of_irreducible, Polynomial.card_roots', Polynomial.IsRoot, Polynomial.dvd_iff_isRoot, Multiset.prod_X_add_C_eq_sum_esymm, Complex.isAlgClosed, Real.goldenRatio_sq, LaurentPolynomial, PowerSeries, MvPolynomial.finSuccEquiv, Polynomial.C_injective, dvd_def, Polynomial.instEuclideanDomain, Irreducible, Polynomial.IsEisensteinAt.irreducible, Nat.ofDigits_digits, Lagrange.interpolate, taylor_mean_remainder, polynomialFunctions_closure_eq_top, Matrix.charpoly, minpoly, Polynomial.instAdd, Polynomial.instMul, Polynomial.rootMultiplicity, Polynomial.Splits.natDegree_eq_card_roots, Polynomial.aeval, Matrix.Pivot.exists_list_transvec_mul_diagonal_mul_list_transvec, Polynomial.divByMonic, solvableByRad.isSolvable, Polynomial.Monic, Polynomial.derivative_C_mul_X_pow |
| Q637347 | Polynomial interpolation | Lagrange.interpolate, Lagrange.eval_interpolate_at_node, Lagrange.eq_interpolate_iff, Lagrange.funEquivDegreeLT, Lagrange.basis, Polynomial.eq_zero_of_degree_lt_of_eval_finset_eq_zero, Matrix.det_vandermonde, Lagrange.eq_interpolate, Lagrange.interpolate_eq_sum |
| Q428971 | Power law | ProbabilityTheory.paretoMeasure |
| Q206925 | Power series | FormalMultilinearSeries, Polynomial.taylor, tsum_geometric_of_norm_lt_one, NormedSpace.exp_eq_tsum, Real.sin_eq_tsum, FormalMultilinearSeries.radius, FormalMultilinearSeries.radius_inv_eq_limsup, FormalMultilinearSeries.ofScalars_radius_eq_inv_of_tendsto, FormalMultilinearSeries.summable_norm_apply, Real.tendsto_tsum_powerSeries_nhdsWithin_lt, HasFPowerSeriesOnBall.add, FormalMultilinearSeries.min_radius_le_radius_add, AnalyticAt.mul, Summable.tsum_mul_tsum_eq_tsum_sum_antidiagonal, PowerSeries.inv, HasFPowerSeriesOnBall.fderiv, AnalyticAt, FormalMultilinearSeries.analyticOnNhd, DifferentiableOn.analyticAt, AnalyticAt.contDiffAt, HasFPowerSeriesOnBall.factorial_smul, HasFPowerSeriesOnBall.hasSum_iteratedFDeriv, AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq, PowerSeries.mk, FormalMultilinearSeries.hasFPowerSeriesOnBall, PowerSeries, MvPowerSeries, PowerSeries.order |
| Q915906 | Presentation of a group | PresentedGroup, FreeGroup, Group.IsFinitelyPresented |
| Q863912 | Prime ideal | Ideal.IsPrime, Ideal.span_singleton_prime, Nat.Prime.dvd_mul, PrimeSpectrum, AlgebraicGeometry.AffineScheme, Ideal.IsPrime.mul_notMem, Ideal.primeCompl, PrincipalIdealRing.isMaximal_of_irreducible, Polynomial.irreducible_of_eisenstein_criterion, Ideal.IsMaximal, Ideal.IsMaximal.isPrime, Ideal.IsPrime.isMaximal_of_ne_bot, MvPolynomial.isMaximal_iff_eq_vanishingIdeal_singleton, Ideal.Quotient.isDomain_iff_prime, Ideal.quotientInfRingEquivPiQuotient, Ideal.isPrime_bot, PrimeSpectrum.isEmpty_iff_subsingleton, Ideal.exists_maximal, Ideal.isPrime_of_maximally_disjoint, Ideal.IsPrime.comap, Ideal.IsMinimalPrime, minimalPrimes.equivIrreducibleComponents, UniqueFactorizationMonoid.iff_exists_prime_mem_of_isPrime, PrimeSpectrum.isIrreducible_iff_vanishingIdeal_isPrime, AlgebraicGeometry.Scheme, IsDedekindDomain, exists_le_isAssociatedPrime_of_isNoetherianRing, Ideal.subset_union_prime, Ideal.IsPrime.inf_le', Ideal.IsOka.isPrime_of_maximal_not, Ideal.isOka_isPrincipal |
| Q49008 | Prime number | Nat.Prime, Nat.prime_two, UniqueFactorizationMonoid.factors_unique, Nat.Prime.eq_two_or_odd', Nat.prime_iff_fac_equiv_neg_one, Nat.fermatNumber, mersenne, Nat.bertrand, Nat.infinite_setOf_prime_and_eq_mod, Nat.factorization, Nat.primeFactors, Nat.Prime.dvd_mul, Nat.exists_infinite_primes, hasSum_zeta_two, not_summable_one_div_on_primes, Nat.primeCounting, RiemannHypothesis, EulerProduct.eulerProduct_hasProd, ZMod, ZMod.instField, ZMod.pow_card, padicValNat, padicNorm, Padic, Rat.AbsoluteValue.equiv_real_or_padic, Prime, Irreducible, Prime.irreducible, Nat.Prime.sq_add_sq, Ideal.IsPrime, Submodule.isLasker, PrimeSpectrum, legendreSym.quadratic_reciprocity, Sylow.exists_subgroup_card_pow_prime, isCyclic_of_prime_card, lucas_lehmer_sufficiency, Nat.primeFactorsList, Polynomial.irreducible_of_eisenstein_criterion |
| Q1570472 | Primitive recursive function | Nat.Primrec, Nat.Primrec', Nat.Primrec'.const, Nat.Primrec'.succ, Nat.Primrec'.get, Nat.Primrec'.comp, Nat.Primrec'.prec, Nat.Primrec'.Vec, Primrec.const, Nat.Primrec'.zero, Primrec.id, Primrec.fst, Nat.Primrec.add, Primrec.nat_double, Nat.Primrec.mul, Nat.Primrec.pred, Nat.Primrec.sub, PrimrecPred, Primrec.eq, Primrec.nat_le, Primrec.cond, PrimrecPred.and, PrimrecPred.or, Primrec.nat_lt, Primrec.nat_casesOn, Primcodable, Nat.Primrec.pow, Primrec.nat_min, Primrec.nat_mod, Primrec.comp, PrimrecRel.comp, PrimrecPred.exists_lt, Primrec.nat_strong_rec, Partrec, Computable, Primrec.to_comp, not_primrec₂_ack, Nat.Primrec'.prim_iff, not_primrec_ack_self, Primrec.nat_iterate, ComputablePred.halting_problem |
| Q2873 | Principal component analysis | LinearMap.IsSymmetric.hasEigenvalue_iSup_of_finiteDimensional |
| Q9492 | Probability | MeasureTheory.prob_le_one, ProbabilityTheory.uniformOn, ProbabilityTheory.gaussianReal, MeasureTheory.MeasureSpace, MeasurableSet, MeasureTheory.IsProbabilityMeasure, MeasureTheory.Measure, MeasureTheory.prob_add_prob_compl, ProbabilityTheory.indepSet_iff_measure_inter_eq_mul, Disjoint, MeasureTheory.measure_union, MeasureTheory.measure_union_add_inter, MeasureTheory.measureReal_biUnion_eq_sum_powerset, ProbabilityTheory.cond, ProbabilityTheory.cond_eq_inv_mul_cond_mul |
| Q207522 | Probability density function | MeasureTheory.pdf, MeasureTheory.HasPDF, MeasureTheory.withDensity_eq_iff_of_sigmaFinite, MeasureTheory.pdf.IsUniform.pdf_eq, ProbabilityTheory.gaussianPDFReal, MeasureTheory.pdf.integral_mul_eq_integral, MeasureTheory.noAtoms_withDensity, MeasureTheory.pdf.indepFun_iff_pdf_prod_eq_pdf_mul_pdf, MeasureTheory.pdf.integral_pdf_smul, ProbabilityTheory.IndepFun.pdf_add_eq_lconvolution_pdf |
| Q7246880 | Probability interpretations | ProbabilityTheory.uniformOn_univ, ProbabilityTheory.strong_law_ae |
| Q623472 | Probability space | MeasureTheory.IsProbabilityMeasure, MeasurableSpace, MeasurableSet, MeasureTheory.ProbabilityMeasure, MeasureTheory.measure_iUnion, MeasureTheory.MeasureSpace, MeasurableSet.univ, MeasurableSet.compl, MeasurableSet.iUnion, MeasurableSet.iInter, MeasureTheory.IsProbabilityMeasure.measure_univ, PMF, MeasureTheory.OuterMeasure.toMeasure, MeasureTheory.Measure.IsComplete, Measurable, MeasureTheory.Measure.map, MeasurableSpace.measurableSet_top, borel, ProbabilityTheory.cond, ProbabilityTheory.cond_isProbabilityMeasure, ProbabilityTheory.IndepSet, ProbabilityTheory.IndepFun, ProbabilityTheory.Indep, Disjoint, MeasureTheory.measure_union, Set.inter |
| Q5862903 | Probability theory | MeasurableSet, MeasureTheory.IsProbabilityMeasure, MeasureTheory.ProbabilityMeasure, ProbabilityTheory.uniformOn, PMF, PMF.toMeasure_apply, ProbabilityTheory.cdf, ProbabilityTheory.monotone_cdf, MeasureTheory.pdf, ProbabilityTheory.cdf_measure_stieltjesFunction, MeasureTheory.Measure, MeasureTheory.Measure.rnDeriv, MeasureTheory.TendstoInDistribution, MeasureTheory.TendstoInMeasure, MeasureTheory.TendstoInMeasure.tendstoInDistribution, ProbabilityTheory.strong_law_ae, ProbabilityTheory.tendstoInDistribution_inv_sqrt_mul_sum_sub, MeasureTheory.IsProbabilityMeasure.measure_univ, MeasureTheory.measure_empty, MeasureTheory.Measure.dirac, MeasurableSpace, borel, MeasureTheory.Measure.count, MeasureTheory.MeasureSpace.volume, ProbabilityTheory.IdentDistrib, MeasureTheory.integral, ProbabilityTheory.variance, ProbabilityTheory.gaussianReal |
| Q901718 | Product (mathematics) | mul_comm, Nat.prod_primeFactorsList, Finset.prod, Finset.prod_empty, ZMod, MeasureTheory.convolution, Real.fourier_mul_convolution_eq, Polynomial.coeff_mul, Module, InnerProductSpace, norm_eq_sqrt_re_inner, InnerProductGeometry.angle, EuclideanSpace.inner_eq_star_dotProduct, crossProduct, triple_product_eq_det, LinearMap, LinearMap.comp, Matrix.instHMulOfFintypeOfMulOfAddCommMonoid, LinearMap.toMatrix_comp, TensorProduct, CategoryTheory.MonoidalCategory, Set.prod, CategoryTheory.CartesianMonoidalCategory |
| Q466720 | Product rule | deriv_mul, deriv_const_mul, logDeriv_mul, iteratedDeriv_mul, IsBoundedBilinearMap.hasFDerivAt, HasDerivAt.smul, HasFDerivAt.inner, Derivation, deriv_pow |
| Q177409 | Projective geometry | Configuration.ProjectivePlane.instDual, Configuration.HasPoints.mkPoint, Configuration.HasPoints, Projectivization.Independent, Configuration.ProjectivePlane |
| Q942423 | Projective module | Module.Projective, Module.Projective.of_free, Module.projective_lifting_property, Module.Projective.iff_split_of_projective, Module.Projective.iff_split, CategoryTheory.Projective.projective_iff_preservesEpimorphisms_preadditiveCoyoneda_obj, Module.projective_def, Module.Projective.of_split, Module.Free.of_divisionRing, Module.projective_of_isSemisimpleRing, Module.Flat.of_projective, Module.Flat.projective_of_finitePresentation, CategoryTheory.ProjectiveResolution, ModuleCat.enoughProjectives, CategoryTheory.projectiveDimension, CategoryTheory.projective_iff_hasProjectiveDimensionLT_one, Module.projective_of_isLocalizedModule, Module.freeLocus_eq_univ_iff, Module.rankAtStalk, Module.isLocallyConstant_rankAtStalk |
| Q1475760 | Projective plane | Configuration.ProjectivePlane, Configuration.ProjectivePlane.order, littleWedderburn, Configuration.Dual, Configuration.ProjectivePlane.instDual, Configuration.ProjectivePlane.card_points_eq_card_lines, Configuration.ProjectivePlane.lineCount_eq_pointCount |
| Q877775 | Projective space | Projectivization.equivSubmodule, projectivizationSetoid, Projectivization, Projectivization.Subspace, Projectivization.Subspace.instInfSet, Projectivization.Subspace.span, Projectivization.Independent, Complex.exists_root, AlgebraicGeometry.Proj, littleWedderburn, Projectivization.map, Matrix.ProjGenLinGroup, Module.Grassmannian |
| Q636716 | Proof that 22/7 exceeds π | intervalIntegral.integral_mul_deriv_eq_deriv_mul |
| Q852732 | Proof theory | Real.exists_isLUB |
| Q200694 | Propositional logic | not_and_or, not_not, not_imp_not, imp_iff_not_or, and_comm, and_assoc, and_or_left, and_imp, Or.resolve_left, mt |
| Q978505 | Pullback (differential geometry) | ContMDiffVectorBundle.pullback, ContinuousMultilinearMap.compContinuousLinearMap, ContinuousAlternatingMap.compContinuousLinearMapCLM, mfderiv, extDeriv_pullback |
| Q837863 | Pure mathematics | irrational_sqrt_two, Function.cantor_surjective, CategoryTheory.Category, CommRing, TopologicalSpace, Group, Matrix, Ring, NormedSpace, Nat.Prime, AlgebraicGeometry.Scheme |
| Q11518 | Pythagorean theorem | EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two, PythagoreanTriple, EuclideanGeometry.angle_add_angle_add_angle_eq_pi, PythagoreanTriple.classification, irrational_sqrt_two, Complex.normSq_apply, Complex.dist_eq, EuclideanSpace.dist_eq, EuclideanSpace.dist_sq_eq, EuclideanGeometry.law_cos, Real.sin_sq_add_cos_sq, EuclideanGeometry.mul_dist_add_mul_dist_eq_mul_dist_of_cospherical, norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero, parallelogram_law_with_norm, OrthogonalFamily.norm_sum, Bundle.RiemannianMetric |
| Q208225 | Pythagorean triple | PythagoreanTriple, PythagoreanTriple.mul, InnerProductGeometry.norm_add_sq_eq_norm_sq_add_norm_sq', PythagoreanTriple.classification, PythagoreanTriple.IsPrimitiveClassified, PythagoreanTriple.coprime_classification, PythagoreanTriple.classified, Matrix.SpecialLinearGroup, GaussianInt, FermatLastTheorem |
| Q41299 | Quadratic equation | Polynomial.roots_quadratic_eq_pair_iff_of_ne_zero, quadratic_eq_zero_iff, Polynomial.natDegree_quadratic, mul_eq_zero, Polynomial.roots_quadratic_eq_pair_iff_of_ne_zero', discrim, quadratic_eq_zero_iff_discrim_eq_sq, Polynomial.dvd_iff_isRoot, quadratic_eq_zero_iff_of_discrim_eq_zero, Real.goldenRatio_sq, Polynomial.eq_neg_mul_add_of_roots_quadratic_eq_pair |
| Q736753 | Quadratic form | QuadraticForm, QuadraticMap.Anisotropic, Nat.Prime.sq_add_sq, Matrix.toQuadraticForm', QuadraticForm.equivalent_weightedSumSquares, QuadraticForm.sigPos_of_equiv_weightedSumSquares, QuadraticForm.discr, QuadraticForm.toMatrix_comp, LinearMap.BilinForm.exists_orthogonal_basis, sigPos, QuadraticMap.PosDef, QuadraticMap.Equivalent, QuadraticMap.associated, QuadraticMap.associated_left_inverse, QuadraticMap, QuadraticMap.map_smul, QuadraticMap.exists_companion, QuadraticMap.IsometryEquiv, LinearMap.BilinMap.toQuadraticMap, QuadraticMap.IsOrtho, Nat.sum_four_squares, MvPolynomial.IsHomogeneous, CliffordAlgebra, QuadraticMap.radical, killingForm, LinearMap.BilinForm.Nondegenerate, Matrix.orthogonalGroup, PythagoreanTriple, Projectivization |
| Q15909572 | Quadratic formula | quadratic_eq_zero_iff, discrim |
| Q50695 | Quadratic function | quadratic_eq_zero_iff, Polynomial.eq_quadratic_of_degree_le_two, QuadraticForm, Nat.iterate |
| Q472883 | Quadratic reciprocity | legendreSym.quadratic_reciprocity, legendreSym.quadratic_reciprocity_one_mod_four, legendreSym.quadratic_reciprocity_three_mod_four, ZMod.exists_sq_eq_neg_one_iff, ZMod.exists_sq_eq_two_iff, ZMod.chineseRemainder, legendreSym.at_neg_one, ZMod.pow_card_sub_one_eq_one, legendreSym, ZMod.exists_sq_eq_neg_two_iff, jacobiSym.quadratic_reciprocity, jacobiSym, instIsCyclicUnitsOfFinite, GaussianInt, ZMod.gauss_lemma, gaussSum, DirichletCharacter.LFunction |
| Q36810 | Quadrilateral | EuclideanGeometry.Cospherical.two_zsmul_oangle_eq, EuclideanGeometry.mul_dist_le_mul_dist_add_mul_dist |
| Q17995793 | Quantum computing | Pell.IsFundamental, Turing.TM0.Machine |
| Q173853 | Quaternion | Quaternion, QuaternionAlgebra.instZero, QuaternionAlgebra.im, Quaternion.finrank_eq_four, QuaternionAlgebra.instMul, Quaternion.instDivisionRing, QuaternionAlgebra.mk_mul_mk, QuaternionAlgebra.Basis.i_mul_k, Subring.center, QuaternionAlgebra.instStarQuaternionAlgebra, star_star, star_mul, Quaternion.star_eq_two_re_sub, Quaternion.self_add_star, Quaternion.normSq, Quaternion.linearIsometryEquivTuple, Quaternion.instNormedAlgebraReal, Quaternion.instNormedDivisionRingReal, Quaternion.instNormedAddCommGroupReal, Quaternion.instInv, QuaternionAlgebra.instAlgebra, QuaternionGroup, Nat.sum_four_squares, Quaternion.exp_eq, QuaternionAlgebra, isSemisimpleRing_iff_pi_matrix_divisionRing, QuaternionAlgebra.coe |
| Q33680 | Radian | Real.Angle.coe_two_pi, Real.isEquivalent_sin, Real.sin_eq_tsum |
| Q918099 | Ramsey's theorem | Finite.exists_infinite_fiber |
| Q176623 | Random variable | Measurable, MeasureTheory.HasPDF, ProbabilityTheory.cdf, MeasureTheory.Measure.map, MeasureTheory.pdf.IsUniform, MeasureTheory.integral, Measurable.comp, ProbabilityTheory.IndepFun.map_mul_eq_map_mconv_map, ProbabilityTheory.IdentDistrib, Filter.EventuallyEq, Eq, PMF, MeasureTheory.pdf, MeasureTheory.Measure.rnDeriv, ProbabilityTheory.variance, ProbabilityTheory.mgf, ProbabilityTheory.strong_law_ae |
| Q856741 | Random walk | ProbabilityTheory.IsBrownianReal |
| Q303402 | Rank–nullity theorem | LinearMap.finrank_range_add_finrank_ker, LinearMap.injective_iff_surjective_of_finrank_eq_finrank, LinearMap.rank_range_add_rank_ker, LinearMap.quotKerEquivRange, Module.Basis.extend |
| Q1783502 | Rate of convergence | Asymptotics.IsBigO, Asymptotics.IsLittleO, Asymptotics.IsTheta, Asymptotics.IsEquivalent, Asymptotics.isBigO_of_div_tendsto_nhds, tendsto_nhds_unique, tendsto_pow_atTop_nhds_zero_of_norm_lt_one, Flow.fromIter, arithGeom_eq |
| Q3481047 | Ratio | Archimedean, Irrational, irrational_sqrt_two, irrational_pi, Real.goldenRatio, tendsto_fib_succ_div_fib_atTop, AffineBasis.coord |
| Q41237 | Rational function | RatFunc, RatFunc.instField, FractionRing, RatFunc.mk, EuclideanDomain.gcd, RatFunc.intDegree, RatFunc.algebraMap_eq_C, RatFunc.coePolynomial, RatFunc.numDenom, RatFunc.X, AlgebraicGeometry.Scheme.functionField |
| Q854531 | Real analysis | ConditionallyCompleteLinearOrderedField, isLUB_csSup, tendsto_atTop_ciSup, intermediate_value_Icc, exists_hasDerivAt_eq_slope, Real.metricSpace, instOrderTopologyReal, Filter.Tendsto, Bornology.IsBounded, Monotone, CauchySeq, Real.instCompleteSpace, tendsto_pi_nhds, TendstoUniformly, TendstoUniformly.continuous, isCompact_cantorSet, Metric.isCompact_iff_isClosed_bounded, IsSeqCompact, isCompact_iff_finite_subcover, IsCompact.isComplete, IsCompact.image, ContinuousOn, Continuous, UniformContinuous, CompactSpace.uniformContinuous_of_continuous, HasDerivAt, DifferentiableAt.continuousAt, ContDiff, AnalyticOn, Summable, hasSum_geometric_of_lt_one, Real.not_summable_one_div_natCast, Summable.of_norm, taylorWithinEval, FormalMultilinearSeries.radius, AnalyticAt, fourierCoeff, BoxIntegral.TaggedPrepartition, BoxIntegral.integralSum, BoxIntegral.integral, intervalIntegral.integral_eq_sub_of_hasDerivAt, MeasureTheory.integral, MeasureTheory.Measure, tendsto_subseq_of_bounded, dense_iInter_of_isOpen, HasDerivAt.lhopital_zero_nhds, taylor_mean_remainder_lagrange, BoundedContinuousFunction.arzela_ascoli, ContinuousMap.subalgebra_topologicalClosure_eq_top_of_separatesPoints, ContractingWith.exists_fixedPoint, HasStrictFDerivAt.localInverse, HasStrictFDerivAt.implicitFunction, MeasureTheory.Egorov.tendstoUniformlyOn_sdiff_iUnionNotConvergentSeq, MeasureTheory.lintegral_liminf_le, MeasureTheory.lintegral_iSup, MeasureTheory.tendsto_integral_of_dominated_convergence, MeasureTheory.integral_prod, MeasureTheory.Measure.absolutelyContinuous_iff_withDensity_rnDeriv_eq, exists_extension_norm_eq, WeakDual.isCompact_polar, InnerProductSpace.toDual, Real.instIsStrictOrderedRing, LinearOrder, Set.sUnion_eq_univ_iff, NormedSpace, InnerProductSpace, EReal, DifferentiableOn, DifferentiableOn.circleIntegral_sub_inv_smul, Complex.exists_root, FormalMultilinearSeries, Real.instField, Real.dist_eq, deriv |
| Q23937546 | Real projective line | Projectivization, Projectivization.equivSubmodule, projectivizationSetoid, Matrix.op_smul_eq_vecMul, Projectivization.generalLinearGroup_smul_def, Matrix.ProjGenLinGroup, OnePoint.smul_some_eq_ite |
| Q740970 | Recurrence relation | LinearRecurrence, Nat.factorial_succ, Nat.fib_add_two, Nat.fib, Nat.choose_succ_succ, Nat.choose_eq_factorial_div_factorial, fwdDiff, LinearRecurrence.charPoly, LinearRecurrence.eq_mk_of_is_sol_of_eq_init, fwdDiff_iter_eq_sum_shift, Nat.choose_symm |
| Q2032198 | Reflexive space | StrongDual, NormedSpace.inclusionInDoubleDual, NormedSpace.inclusionInDoubleDualLi |
| Q1930388 | Register machine | Turing.TM0.Machine, Nat.Partrec, Nat.Primrec, ack |
| Q1135405 | Regression toward the mean | ProbabilityTheory.strong_law_ae |
| Q752532 | Regular language | Language.IsRegular, NFA.reverse |
| Q389208 | Repeating decimal | Irrational, ZMod.pow_card_sub_one_eq_one, orderOf, ArithmeticFunction.pow_carmichael |
| Q13220368 | Representation theory | MulAction, Representation, Rep.V, Representation.IntertwiningMap, Representation.Equiv, Subrepresentation, Representation.IsIrreducible, FDRep.finrank_hom_simple_simple, Representation.directSum, Representation.IsSemisimpleRepresentation, Representation.tprod, MonoidAlgebra.Submodule.exists_isCompl, FDRep.character, LieGroup, LieAlgebra, Action |
| Q3526854 | Representation theory of finite groups | Representation, LinearMap.GeneralLinearGroup, Representation.trivial, Representation.ofMulAction, Representation.leftRegular, MonoidAlgebra, Representation.IntertwiningMap.equivLinearMapAsModule, Representation.IntertwiningMap, Subrepresentation, Representation.IsIrreducible, Representation.IsIrreducible.bijective_or_eq_zero, Representation.Equiv, Rep.res, Representation.IsSemisimpleRepresentation, DihedralGroup, Representation.dual, Representation.directSum, Representation.tprod, MonoidAlgebra.Submodule.exists_isCompl, Representation.isProj_averageMap, FDRep.character, FDRep.char_conj, Matrix.trace_mul_comm, FDRep.char_one, FDRep.char_orthonormal, Representation.ind, SemidirectProduct, YoungDiagram, IsTopologicalGroup, ContRepresentation, MeasureTheory.Measure.isHaarMeasure_eq_of_isProbabilityMeasure |
| Q7322955 | Ricci calculus | contractLeft, Module.Basis.ext_elem_iff, MultilinearMap.alternatization, fderiv_mul, CovariantDerivative, IsCovariantDerivativeOn.leibniz, extDeriv, VectorField.mlieBracket_self, Matrix.one_apply, CovariantDerivative.torsion |
| Q205966 | Riemann hypothesis | RiemannHypothesis, zeta_eq_tsum_one_div_nat_cpow, riemannZeta_eulerProduct_tprod, riemannZeta_one_sub, riemannZeta_neg_two_mul_nat_add_one, riemannZeta_zero, ArithmeticFunction.moebius, ArithmeticFunction.sigma, riemannZeta_ne_zero_of_one_le_re, ArithmeticFunction.liouville, Real.eulerMascheroniConstant, harmonic, Nat.totient, riemannZeta_two, Nat.primeCounting, Chebyshev.psi, DirichletCharacter.LFunction |
| Q825857 | Riemann sphere | onePointEquivSphereOfFinrankEq, OnePoint.equivProjectivization, stereographic, MeromorphicOn, MDifferentiable.exists_eq_const_of_compactSpace |
| Q753035 | Riemann surface | MDifferentiable.comp, MDifferentiable.exists_eq_const_of_compactSpace |
| Q187235 | Riemann zeta function | riemannZeta, differentiableAt_riemannZeta, riemannZeta_residue_one, riemannZeta_eulerProduct_tprod, Nat.exists_infinite_primes, not_summable_one_div_on_primes, riemannZeta_one_sub, completedRiemannZeta_one_sub, RiemannHypothesis, riemannZeta_ne_zero_of_one_le_re, riemannZeta_two_mul_nat, riemannZeta_two, riemannZeta_neg_nat_eq_bernoulli, riemannZeta_neg_two_mul_nat_add_one, riemannZeta_zero, ArithmeticFunction.LSeries_zeta_mul_Lseries_moebius, mellin, HurwitzZeta.hurwitzZeta |
| Q632814 | Riemannian manifold | IsRiemannianManifold, Bundle.ContMDiffRiemannianMetric, Bundle.RiemannianMetric, IsContMDiffRiemannianBundle, riemannianMetricVectorSpace, Metric.diam, CovariantDerivative, CovariantDerivative.IsMetricCompatible, CovariantDerivative.torsion_eq_zero_iff, TangentSpace, Bundle.RiemannianMetric.toCore, Manifold.riemannianEDist |
| Q1357684 | Riesz representation theorem | InnerProductSpace.toDual, HilbertSpace, LinearMap, IsBoundedLinearMap.isLinearMap_and_continuous_iff_isBoundedLinearMap, ContinuousLinearEquiv.symm, LinearMap.comp, StrongDual, ContinuousLinearMap, InnerProductSpace, real_inner_comm, ContinuousLinearMap.le_opNorm, inner_eq_zero_symm, Submodule.mem_orthogonal', Submodule.isClosed_orthogonal, Submodule.HasOrthogonalProjection.ofCompleteSpace, InnerProductSpace.toDualMap, innerSL_apply_norm, innerSL_inj, inner_self_nonneg, inner_self_eq_zero, InnerProductSpace.toDual_symm_apply, Matrix.toEuclideanLin_conjTranspose_eq_adjoint, InnerProductSpace.rclikeToReal, innerSLFlip, ContinuousLinearMap.adjoint, LinearMap.toMatrix_adjoint, Module.Dual.transpose, ContinuousLinearMap.isSelfAdjoint_iff', ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric, ContinuousLinearMap.isStarNormal_iff_norm_eq_adjoint, Unitary.linearIsometryEquiv, Unitary.inner_map_map, LinearEquiv.dualMap |
| Q161172 | Ring (mathematics) | Ring, CommRing, NonUnitalRing, DivisionRing, Int.instCommRing, ZMod, Matrix.instRing, Rat.instField, Algebra, Polynomial, ContinuousMap.instCommRingOfIsTopologicalRing, Pi.ring, AddMonoid.End, MonoidAlgebra, Finset.prod, Monoid.npow, IsNilpotent, IsIdempotentElem, IsUnit, Subring, Subring.instCompleteLattice, Subring.closure, Subring.center, Ideal.span, IsSimpleRing, isSimpleRing_iff_isField, IsNoetherianRing, IsSemiprimaryRing.isNoetherian_iff_isArtinian, Ideal.IsPrime, RingHom, RingEquiv, Int.castRingHom, frobenius, AlgEquiv, Representation, RingHom.ker, Ideal.Quotient.mk, Ideal.Quotient.lift, RingHom.quotientKerEquivOfSurjective, Module, Module.compHom, Prod.instRing, Ideal.quotientInfRingEquivPiQuotient, Polynomial.instIsDomainOfIsCancelAdd, Polynomial.aeval, MvPolynomial.aeval_unique, MvPolynomial.vanishingIdeal_zeroLocus_eq_radical, PowerSeries, Module.End, Matrix.toLinAlgEquiv, Module.End.instDivisionRing, IsSemisimpleRing.exists_algEquiv_pi_matrix_divisionRing, Ring.DirectLimit, Localization, LocalizedModule, IsLocalization.orderIsoOfPrime, IsLocalizedModule.map_exact, AdicCompletion, Ideal.iInf_pow_eq_bot_of_isDomain, PadicInt, padicNorm, FreeRing, FreeRing.lift, Algebra.TensorProduct.instAlgebra, IsDomain, IsPrincipalIdealRing, UniqueFactorizationMonoid, Module.equiv_free_prod_directSum, littleWedderburn, Module.Free.of_divisionRing, IsSemisimpleModule, DivisionRing.toIsSemisimpleRing, IsSemisimpleRing.instMatrix, MonoidAlgebra.Submodule.exists_isCompl, IsSemisimpleRing.isSemisimpleModule, Algebra.IsCentralSimple, Brauer.CSA_Setoid, BrauerGroup, IsAzumaya, Valuation, ValuationSubring, IsTopologicalRing, IsOrderedRing, NonUnitalNonAssocRing, Semiring, Nat.instCommSemiring |
| Q1208658 | Ring theory | CommRing, IsDomain, IsPrincipalIdealRing, EuclideanDomain, MvPolynomial.isMaximal_iff_eq_vanishingIdeal_singleton, PrimeSpectrum, Module, Matrix.instRing, IsSimpleRing.exists_ringEquiv_matrix_divisionRing, jacobson_density, IsSemiprimaryRing.isNoetherian_iff_isArtinian, littleWedderburn, ringKrullDim, MvPolynomial.ringKrullDim_of_isNoetherianRing, IsMoritaEquivalent, CommRing.Pic, Ring.jacobson, Quaternion, MvPolynomial.IsSymmetric, MvPolynomial.esymmAlgEquiv |
| Q534131 | Root system | RootPairing.IsRootSystem, RootPairing.IsCrystallographic, RootPairing.IsReduced, RootPairing.IsIrreducible, RootPairing.Equiv, RootPairing.rootSpan, RootPairing.weylGroup, LieAlgebra.IsKilling.rootSystem, RootPairing.pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed, RootPairing.Base, RootPairing.Base.toWeightBasis, RootPairing.coroot, RootPairing.flip, RootPairing.flip_flip, RootPairing.corootSpan, RootPairing.Base.flip, LieAlgebra.IsKilling.isSimple_iff_isIrreducible, RootPairing.InvariantForm.exists_apply_eq_or, RootPairing.mapsTo_reflection_root, RootPairing.Base.cartanMatrix |
| Q126736 | Scalar multiplication | Module, SameRay.sameRay_pos_smul_right, add_smul, smul_add, mul_smul, one_smul, zero_smul, neg_one_smul, Units.instGroup, Units.instDistribMulAction, norm_smul_of_nonneg, sameRay_neg_smul_right_iff_of_ne, Semiring.toModule, smul_eq_mul, Pi.module, Pi.smul_apply, op_smul_eq_mul, Matrix.smul_apply, Matrix.op_smul_eq_mul_diagonal, Matrix.smul_eq_mul_diagonal |
| Q165498 | Schrödinger equation | Module.End.HasEigenvector, MeasureTheory.pdf |
| Q1548746 | Second-order logic | ConditionallyCompleteLinearOrderedField.inducedOrderRingIso |
| Q6500908 | Self-adjoint operator | IsSelfAdjoint, LinearMap.IsSymmetric.eigenvectorBasis_apply_self_apply, LinearPMap.graph, LinearPMap.adjoint, LinearMap.IsSymmetric, LinearPMap.isSelfAdjoint_def, LinearMap.IsSymmetric.continuous, ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric, realPart_add_I_smul_imaginaryPart, ContinuousLinearMap.IsPositive.isSelfAdjoint, ContinuousLinearMap.norm_eq_iSup_rayleighQuotient, LinearMap.IsSymmetric.conj_eigenvalue_eq_self, ContinuousLinearMap.eq_zero_of_forall_hasEigenvalue_eq_zero, resolventSet, spectrum, IsSelfAdjoint.val_re_map_spectrum, QuasispectrumRestricts.isSelfAdjoint, LinearMap.IsSymmetric.eigenvectorBasis, cfc, MeasureTheory.Measure.MutuallySingular |
| Q680081 | Separable space | TopologicalSpace.SeparableSpace, Continuous.ext_on, TopologicalSpace.Countable.to_separableSpace, TopologicalSpace.separableSpace_iff_countable, TopologicalSpace.SecondCountableTopology.to_separableSpace, TopologicalSpace.isSeparable_range, exists_extension_norm_eq, IsCompact.isSeparable, TopologicalSpace.IsSeparable.iUnion, ContinuousMap.instSeparableSpace, Topology.IsOpenEmbedding.separableSpace, TopologicalSpace.IsSeparable.of_separableSpace, IsClosed.mk_lt_continuum, Metric.PiNatEmbed.exists_embedding_to_hilbert_cube, KuratowskiEmbedding.exists_isometric_embedding |
| Q1140985 | Separation axiom | SeparatedNhds, T0Space, R0Space, T1Space, t1Space_iff_t0Space_and_r0Space, R1Space, instR0Space, T2Space, R1Space.t2Space_iff_t0Space, T2Space.t1Space, T25Space, T25Space.t2Space, RegularSpace, instR1Space, T3Space, T3Space.t25Space, CompletelyRegularSpace, CompletelyRegularSpace.instRegularSpace, T35Space, NormalSpace, NormalSpace.instCompletelyRegularSpace, T4Space, T4Space.instT35Space, CompletelyNormalSpace, CompletelyNormalSpace.toNormalSpace, T5Space, T5Space.toT4Space, PerfectlyNormalSpace.toCompletelyNormalSpace, T6Space, T6Space.toT5Space |
| Q133250 | Sequence | Stream'.Seq, List.length, FreeMonoid, List.nil, Nat.Prime, Nat.nth, Nat.fib, Rat.denseRange_cast, Real.digits, Polynomial.basisMonomials, Nat.fib_add_two, LinearRecurrence, Stream', List, Monotone, Antitone, StrictMono, BddAbove, upperBounds, BddBelow, Bornology.IsBounded, ArithmeticFunction.IsMultiplicative, Filter.Tendsto, tendsto_nhds_unique, Metric.tendsto_atTop, Filter.Tendsto.mul, le_of_tendsto_of_tendsto, tendsto_of_tendsto_of_tendsto_of_le_of_le, tendsto_atTop_ciSup, Filter.tendsto_of_subseq_tendsto, CauchySeq, cauchySeq_tendsto_of_complete, CompleteSpace, tsum, Finset.sum, HasSum, isCompact_iff_isSeqCompact, continuous_iff_seqContinuous, TopologicalSpace.exists_dense_seq, Filter, Pi.topologicalSpace, continuous_apply, lp, Pi.module, FreeSemigroup, Function.Exact, String, cantorSetHomeomorphNatToBool |
| Q36161 | Set (mathematics) | Set, Set.Mem, Set.ext, Set.instEmptyCollection, Set.singleton, Set.Finite, Set.Infinite, instInfiniteNat, Mathlib.Meta.setBuilder, Set.Subset, Set.instHasSSubset, Set.Subset.antisymm_iff, Set.empty_subset, Set.inter, Set.inter_assoc, Set.sInter, Set.union, Set.union_assoc, Set.sUnion, Set.diff, Set.compl, symmDiff, Set.powerset, Set.instBooleanAlgebra, Set.instCompleteAtomicBooleanAlgebra, Set.image, Function.graph, Set.prod, Set.pi, Classical.axiomOfChoice, Pi, Cardinal.mk_powerset, Sum, Sigma, Setoid.IsPartition, Cardinal.mk, Cardinal.eq, Cardinal.instLE, Function.Embedding.schroeder_bernstein, Cardinal.linearOrder, Set.Countable, Function.cantor_surjective, Cardinal.continuum, Cardinal.mk_real, Cardinal.mk_complex, IsChain, zorn_le, Module.Basis.ofVectorSpace, Ideal.exists_le_maximal, WellOrderingRel, Nat.lt_wfRel, Ordinal.induction |
| Q12482 | Set theory | Cardinal, Cardinal.not_countable_real, Function.cantor_surjective, Cardinal.cantor, Ordinal, Cardinal.aleph, Ordinal.omega0, Setoid, Setoid.IsPartition, Classical.choice, Set.Mem, Set.Subset, Set.ssubset_iff_subset_ne, Set.union, Set.inter, Set.diff, Set.compl, symmDiff, Set.prod, Set.instEmptyCollection, Set.powerset, ZFSet.rank, borel, Nat, Int, Real |
| Q33100 | Seven Bridges of Königsberg | SimpleGraph.Walk.IsTrail.even_countP_edges_iff, SimpleGraph.Walk.IsEulerian.even_degree_iff, SimpleGraph.degree, SimpleGraph.Walk.IsEulerian, SimpleGraph, SimpleGraph.ext, SimpleGraph.Walk, SimpleGraph.Connected, SimpleGraph.Walk.IsTrail |
| Q595298 | Sheaf (mathematics) | TopCat.Presheaf, TopCat.presheafToTop, TopCat.Presheaf.IsSheaf, CategoryTheory.Presheaf.IsSeparated, TopCat.sheafToTop, AlgebraicGeometry.structureSheafInType, TopCat.Presheaf.isSheaf_iff_isSheafPairwiseIntersections, skyscraperSheaf, CategoryTheory.Sheaf, TopCat.Presheaf.isIso_iff_stalkFunctor_map_iso, TopCat.Presheaf.stalk, TopCat.Presheaf.germ, CategoryTheory.sheafify, CategoryTheory.constantSheaf, CategoryTheory.sheafificationAdjunction, CategoryTheory.sheafHom, TopCat.Presheaf.pushforward, TopCat.Sheaf.pullback, CategoryTheory.Presheaf.isSheaf_iff_isLimit, AlgebraicGeometry.RingedSpace, AlgebraicGeometry.LocallyRingedSpace, AlgebraicGeometry.Scheme, SheafOfModules, TopCat.Sheaf.pullbackPushforwardAdjunction, CategoryTheory.GrothendieckTopology |
| Q940334 | Shor's algorithm | orderOf, sq_sub_sq, Real.exists_rat_eq_convergent |
| Q208163 | Signal processing | convolution |
| Q1056761 | Significant figures | irrational_pi, Real.logb |
| Q206816 | Simple continued fraction | SimpContFract, GenContFract.partDens, GenContFract.terminates_iff_rat, ContFract, GenContFract.contsAux, GenContFract.of_convergence, GenContFract.IntFractPair.stream, GenContFract.of, GenContFract.convs, GenContFract.conts_recurrence, SimpContFract.determinant, Real.exists_convs_eq_rat, GenContFract |
| Q331350 | Simplex | Affine.Simplex, Affine.Simplex.mkOfPoint, stdSimplex_fin_two, Affine.Triangle, stdSimplex, Geometry.SimplicialComplex, AbstractSimplicialComplex, Affine.Simplex.face, single_mem_stdSimplex, AffineBasis.coord, stdSimplex_unique, MeasureTheory.Measure.addHaar_parallelepiped, TopCat.toSSetObjEquiv, CategoryTheory.SimplicialObject |
| Q420904 | Singular value decomposition | LinearMap.singularValues, LinearMap.card_support_singularValues, LinearMap.IsSymmetric.hasEigenvalue_iSup_of_finiteDimensional, Matrix.IsHermitian.spectral_theorem, Matrix.frobenius_norm_def, Matrix.unitaryGroup, Matrix.orthogonalGroup, Matrix.conjTranspose, LinearMap.finrank_range_add_finrank_ker, IsCompact.exists_isMaxOn, LinearMap.range, LinearMap.ker, Matrix.PosSemidef, IsCompactOperator, ContinuousLinearMap.opNorm |
| Q190667 | Slide rule | Real.log_mul, quadratic_eq_zero_iff, Real.logb, div_add_one |
| Q1501536 | Sobolev space | TemperedDistribution.MemSobolev, MeasureTheory.MemLp.indicator |
| Q759832 | Solvable group | IsSolvable, derivedSeries, Group.instIsSolvable, IsNilpotent.to_isSolvable, solvable_of_ker_le_range, Equiv.Perm.fin_5_not_solvable, Equiv.Perm.not_solvable, IsZGroup, Group.instIsSolvableSubtypeMemSubgroup, solvable_of_surjective, Group.instIsSolvableProd |
| Q133327 | Spacetime | EuclideanSpace.dist_eq, Isometry.dist_eq, IsRiemannianManifold |
| Q684363 | Special unitary group | Matrix.specialUnitaryGroup, Matrix.unitaryGroup |
| Q3503315 | Spectral sequence | CategoryTheory.CohomologicalSpectralSequence, CategoryTheory.SpectralSequence.page, CategoryTheory.SpectralSequence, CategoryTheory.SpectralSequence.Hom, HomologicalComplex₂, HomologicalComplex₂.total, CategoryTheory.CohomologicalSpectralSequenceNat |
| Q1425077 | Spectral theorem | Matrix.IsHermitian.spectral_theorem, LinearMap.IsSymmetric, ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric, LinearMap.IsSymmetric.conj_eigenvalue_eq_self, Module.End.HasEigenvector, Complex.isAlgClosed, LinearMap.IsSymmetric.direct_sum_isInternal, Module.End.eigenspace, LinearMap.IsSymmetric.eigenvectorBasis_apply_self_apply, IsStarNormal, ContinuousLinearMap.orthogonalComplement_iSup_eigenspaces_eq_bot, cfc |
| Q2409122 | Spectral theory | resolventSet, spectrum, resolvent, Module.End.HasEigenvalue.mem_spectrum, IsSelfAdjoint.mem_spectrum_eq_re, InnerProductSpace.rankOne, Module.End.HasEigenvalue, OrthonormalBasis.sum_rankOne_eq_id, OrthonormalBasis.sum_repr', IsSelfAdjoint.hasEigenvector_of_isMaxOn |
| Q12507 | Sphere | Metric.sphere, EuclideanGeometry.Sphere, Metric.closedBall, frontier_closedBall, EuclideanSpace.volume_ball, isCompact_sphere |
| Q900117 | Sphere packing | Fourier.fourierIntegral, hammingDist |
| Q203218 | Spherical coordinate system | Metric.sphere |
| Q877100 | Spherical harmonics | InnerProductSpace.HarmonicAt, MvPolynomial.IsHomogeneous |
| Q164 | Square | irrational_sqrt_two, IsSquare, DihedralGroup, InnerProductGeometry.norm_add_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two |
| Q134237 | Square root | IsSquare, Real.sqrt, sq_eq_sq_iff_eq_or_eq_neg, irrational_sqrt_ratCast_iff_of_nonneg, Real.sqrt_sq_eq_abs, Real.sqrt_mul, Real.continuous_sqrt, Nat.sqrt_eq, irrational_sqrt_natCast_iff, Complex.I, Complex.sqrt_neg_of_nonneg, Complex.sqrt, Complex.differentiableOn_sqrt, Complex.sqrt_eq_real_add_ite, Complex.sqrt_I, Polynomial.IsRoot, CFC.sqrt_unique, frobenius_inj |
| Q389813 | Square root of 2 | Real.sqrt, irrational_sqrt_two, irrational_sqrt_natCast_iff, Real.cos_pi_div_four |
| Q193394 | Squaring the circle | EuclideanSpace.volume_ball_fin_two, intermediate_value_Icc, integral_inv, irrational_pi, Complex.exp_pi_mul_I, Real.goldenRatio |
| Q159375 | Standard deviation | ProbabilityTheory.variance, ProbabilityTheory.variance_eq_sub, ProbabilityTheory.meas_ge_le_variance_div_sq, ProbabilityTheory.IndepFun.variance_sum, ProbabilityTheory.covariance |
| Q7598372 | Standard probability space | MeasureTheory.Measure.map, MeasurableSpace.CountablySeparated, MeasurableSpace.CountablyGenerated, MeasureTheory.Measure.condKernel |
| Q2500758 | Stationary point | IsLocalMin, IsLocalMax, IsLocalExtr, IsExtrOn, IsLocalExtr.deriv_eq_zero, isLocalMin_of_deriv_deriv_pos |
| Q210832 | Statistical hypothesis test | Measurable, ProbabilityTheory.cond |
| Q12483 | Statistics | ProbabilityTheory.IdentDistrib, ProbabilityTheory.gaussianReal |
| Q866099 | Stereographic projection | stereographic, Metric.sphere, stereographic_apply, stereographic', stereographic_source, onePointEquivSphereOfFinrankEq, circleEquivGen, Real.sin_eq_two_mul_tan_half_div_one_add_tan_half_sq |
| Q80918 | Stirling number | Nat.stirlingFirst, Nat.stirlingSecond, descPochhammer_zero, Ring.descPochhammer_eq_factorial_smul_choose |
| Q176737 | Stochastic process | ProbabilityTheory.isProjectiveLimit_map, ProbabilityTheory.isProjectiveMeasureFamily_map_restrict, MeasureTheory.Filtration, ProbabilityTheory.IndepFun.process_indepFun_process, MeasureTheory.Martingale, MeasureTheory.Submartingale.ae_tendsto_limitProcess, MeasureTheory.Measure.isProjectiveLimit_infinitePi |
| Q939927 | Stone–Weierstrass theorem | polynomialFunctions_closure_eq_top, bernsteinApproximation_uniform, ContinuousMap.instSeparableSpace, ContinuousMap.instNormedAlgebra, Subalgebra.SeparatesPoints, ContinuousMap.subalgebra_topologicalClosure_eq_top_of_separatesPoints, ZeroAtInftyContinuousMap, StarAlgebra.adjoin, fourierSubalgebra_closure_eq_top, ContinuousMap.starSubalgebra_topologicalClosure_eq_top_of_separatesPoints, ContinuousMap.instLatticeOfTopologicalLattice, ContinuousMap.sublattice_closure_eq_top, NormedAlgebra, ContinuousMap.instCStarRing |
| Q33198 | String theory | Matrix, Group, DihedralGroup, IsSimpleGroup, IsSimpleModule, fourierCoeff, Real.Gamma, Real.log |
| Q1851710 | Structure (mathematical logic) | FirstOrder.Language.Structure, FirstOrder.Language.Theory.Model, FirstOrder.Language, FirstOrder.Language.IsAlgebraic, FirstOrder.Language.Constants, FirstOrder.Language.ring, FirstOrder.Language.Substructure, FirstOrder.Language.ClosedUnder, FirstOrder.Language.Substructure.closure, FirstOrder.Language.Substructure.mem_closed_iff, FirstOrder.Language.Substructure.instCompleteLattice, SimpleGraph.structure, FirstOrder.Language.Hom, FirstOrder.Language.StrongHomClass, FirstOrder.Language.Embedding, FirstOrder.Language.StrongHomClass.toEmbedding, FirstOrder.Language.BoundedFormula.Realize, Set.Definable, Set.Definable.singleton |
| Q1154082 | Sturm–Liouville theory | IsPicardLindelof.exists_eq_forall_mem_Icc_hasDerivWithinAt |
| Q177646 | Subset | Set.Subset, Set.ssubset_def, Set.powersetCard, Set.subset_def, Set.ssubset_iff_subset_ne, Set.empty_subset, Set.Subset.refl, Set.Subset.trans, Set.Subset.antisymm, lt_irrefl, lt_trans, lt_asymm, Set.powerset, Set.instBooleanAlgebra, OrderDual, Set.inter_eq_left, Set.union_eq_right, Set.le_eq_subset, Ordinal |
| Q40754 | Subtraction | SubNegMonoid, sub_eq_add_neg, neg_sub, sub_zero, Order.pred |
| Q484298 | Surface (topology) | chartAt, ModelWithCorners.IsBoundaryPoint, ModelWithCorners.IsInteriorPoint, exists_embedding_euclidean_of_compact |
| Q229102 | Surjective function | Function.Surjective, Function.surjective_id, Real.log_surjective, Prod.fst_surjective, Function.Bijective, Function.RightInverse, Function.surjective_iff_hasRightInverse, Set.image_preimage_eq, Function.injective_comp_right_iff_surjective, CategoryTheory.epi_iff_surjective, CategoryTheory.IsSplitEpi.epi, CategoryTheory.SplitEpi.section_, CategoryTheory.IsSplitEpi, Cardinal.mk_le_of_surjective, Finite.injective_iff_surjective_of_equiv, Function.Surjective.comp, Set.rangeFactorization_surjective, Setoid.quotientKerEquivOfSurjective |
| Q1057919 | Sylow theorems | IsPGroup, Sylow, Subgroup.card_subgroup_dvd_card, Sylow.card_eq_multiplicity, Sylow.nonempty, exists_prime_orderOf_dvd_card, Sylow.isPretransitive_of_finite, card_sylow_modEq_one, Sylow.exists_subgroup_card_pow_prime, Sylow.normal_of_subsingleton, Sylow.card_dvd_index, IsPGroup.exists_le_sylow, Nat.prime_iff_fac_equiv_neg_one, Sylow.normalizer_sup_eq_top, MonoidHom.ker_transferSylow_isComplement', Subgroup.commutator_inf_eq_focalSubgroup, IsPGroup.card_modEq_card_fixedPoints, MulAction.card_orbit_mul_card_stabilizer_eq_card_group, Sylow.exists_subgroup_card_pow_succ |
| Q849512 | Symmetric group | Equiv.Perm, Fintype.card_perm, Equiv.Perm.subgroupOfMulAction, Equiv.permUnique, Equiv.Perm.permGroup, Equiv.Perm.mul_apply, Equiv.Perm.IsSwap, Equiv.Perm.closure_isSwap, Equiv.Perm.sign, Equiv.Perm.sign_prod_list_swap, Equiv.Perm.sign_mul, alternatingGroup, alternatingGroup.index_eq_two, Equiv.Perm.mclosure_swap_castSucc_succ, Equiv.Perm.IsCycle, Equiv.Perm.IsCycle.orderOf, Equiv.Perm.card_support_eq_two, Equiv.Perm.Disjoint, Equiv.Perm.Disjoint.commute, Equiv.Perm.truncCycleFactors, Fin.revPerm, Fin.rev_rev, Equiv.Perm.isConj_iff_cycleType_eq, Equiv.Perm.partition, Equiv.Perm.fin_5_not_solvable, alternatingGroup.isSimpleGroup, Subgroup, Equiv.Perm.isCoatom_stabilizer, Sylow.isPGroup', IteratedWreathProduct, MulAction.IsPretransitive, Polynomial.Gal.galAction_isPretransitive, Subgroup.zpowers, Equiv.Perm.lcm_cycleType, MonoidAlgebra.Submodule.instIsSemisimpleModule, List.formPerm, Equiv.Perm.cycleType, RegularWreathProduct |
| Q12485 | Symmetry | Symmetric, And.symm, Module.involutive_reflection, Equiv.pointReflection_involutive |
| Q21030012 | Symmetry (geometry) | MulAction.stabilizer, AffineIsometryEquiv.pointReflection |
| Q2431134 | Symmetry in mathematics | Function.Even, Function.Odd, Matrix.IsSymm, Matrix.IsSymm.apply, Matrix.isSymm_diagonal, Matrix.isHermitian_iff_isSymmetric, Equiv.Perm, Fintype.card_perm, MvPolynomial.IsSymmetric, MvPolynomial.esymmAlgHom_surjective, SymmetricPower, Polynomial.Gal.galActionHom, CategoryTheory.Aut, MulAut, LinearMap.GeneralLinearGroup, RingAut, LinearMap.BilinForm.IsAlt.neg_eq, Symmetric, Isometry, Congruent |
| Q11203 | System of linear equations | Matrix.mulVec_eq_sum, Matrix.mulVec, Matrix.mulVec_cramer, Matrix.inv_mulVec_eq_vec, Matrix.mulVec_zero, Matrix.mulVec_add, Matrix.mulVecLin, LinearMap.sub_mem_ker_iff, LinearMap.mem_range |
| Q131251 | Tangent | slope, hasDerivAt_iff_tendsto_slope, DifferentiableAt.continuousAt, TangentSpace, PointDerivation, EuclideanGeometry.Sphere.IsExtTangent, EuclideanGeometry.Sphere.isExtTangent_iff_dist_center |
| Q746550 | Tangent bundle | TangentBundle, Bundle.TotalSpace.mk, Bundle.TotalSpace.proj, ContMDiff.contMDiff_tangentMap, tangentBundleCore, TangentSpace.vectorBundle, ContMDiffSection, TangentSpace, ContMDiffSection.instAdd |
| Q909601 | Tangent space | TangentSpace, range_mfderiv_coe_sphere, TangentBundle, ContMDiff, ContMDiffMap.algebra, Derivation, Derivation.map_algebraMap, PointDerivation, NormedSpace.fromTangentSpace, lineDeriv, tangentMap |
| Q131187 | Taylor series | taylorWithin, HasFPowerSeriesAt.comp, FormalMultilinearSeries.radius_le_radius_derivSeries, taylor_mean_remainder_lagrange, shift_eq_sum_fwdDiff_iter, expNegInvGlue, taylor_tendsto, AnalyticAt, Complex.taylorSeries_eq_on_ball, DifferentiableOn.analyticAt, FormalMultilinearSeries.radius_eq_liminf, MeromorphicAt, NormedSpace.exp_eq_tsum, Real.hasSum_pow_div_log_of_abs_lt_one, hasSum_geometric_of_norm_lt_one, binomialSeries, Complex.cos_eq_tsum, Complex.cosh_eq_tsum |
| Q1137206 | Taylor's theorem | taylor_mean_remainder_lagrange, hasDerivAt_iff_isLittleO, taylorWithinEval, taylor_isLittleO, taylorWithin, taylor_mean_remainder, taylor_integral_remainder, taylor_mean_remainder_bound, exists_taylor_mean_remainder_bound, AnalyticAt, FormalMultilinearSeries.radius_inv_eq_limsup, HasFPowerSeriesOnBall.tendstoUniformlyOn, expNegInvGlue.not_analyticAt_zero, DifferentiableOn.analyticOnNhd, Complex.circleIntegral_div_sub_of_differentiable_on_off_countable, DifferentiableOn.contDiffOn, Complex.norm_iteratedDeriv_le_of_forall_mem_sphere_norm_le, HasFDerivAt, fderiv |
| Q188524 | Tensor | TensorProduct, dualTensorHomEquiv, MultilinearMap, Module.evalEquiv, PiTensorProduct.lift, dotProductBilin, LinearMap.BilinForm, TensorAlgebra, TensorProduct.addCommMonoid, TensorProduct.tmul, contractLeft, PiTensorProduct |
| Q1163016 | Tensor product | TensorProduct, TensorProduct.tmul, TensorProduct.lift.equiv, Module.Basis.tensorProduct, Module.Basis.tensorProduct_apply, Submodule.LinearDisjoint, Module.finrank_tensorProduct, TensorProduct.assoc, TensorProduct.comm, TensorProduct.map, TensorProduct.map_surjective, TensorProduct.toMatrix_map, TensorAlgebra, contractLeft, coevaluation, dualTensorHomEquiv, TensorProduct.mk, LinearMap.rTensor_surjective, Algebra.TensorProduct.instAlgebra, Algebra.IsAlgebraic.tensorProduct, MultilinearMap.domCoprod, ExteriorAlgebra, ExteriorAlgebra.exteriorPower, SymmetricAlgebra, CategoryTheory.MonoidalCategory, Matrix.kroneckerMap, TensorProduct.directSum, Finsupp |
| Q214856 | Tessellation | DiscreteTiling.Prototile |
| Q160003 | Tetrahedron | Affine.Simplex, Affine.Simplex.circumsphere, Affine.Simplex.Regular, Affine.Simplex.mongePoint, Affine.Simplex.dist_point_centroid, Affine.Simplex.ninePointCircle, Affine.Simplex.ninePointCircle_radius |
| Q65943 | Theorem | EuclideanGeometry.angle_add_angle_add_angle_eq_pi, FermatLastTheorem, even_iff_two_dvd, FirstOrder.Language.Theory, FirstOrder.Language.Sentence |
| Q1154787 | Theta function | jacobiTheta₂, jacobiTheta₂_add_left', jacobiTheta₂_add_left, jacobiTheta_S_smul, jacobiTheta₂_functional_equation, Complex.betaIntegral, Complex.betaIntegral_eq_Gamma_mul_div, Nat.Partition, Nat.Partition.hasProd_powerSeriesMk_card_restricted, pentagonal, Nat.Partition.distincts, Nat.Partition.hasProd_powerSeriesMk_card_countRestricted |
| Q2393193 | Time complexity | Asymptotics.IsBigO, Int.floor, Turing.TM2ComputableInPolyTime, Nat.factorial, Stirling.tendsto_stirlingSeq_sqrt_pi |
| Q737279 | Timeline of mathematics | irrational_sqrt_two, Nat.exists_infinite_primes, ZMod.chineseRemainder, Real.sin, sq_add_sq_mul_sq_add_sq, EuclideanSpace.volume_ball, Real.arctan, add_pow, fermatLastTheoremThree, EuclideanGeometry.law_sin, Nat.rec, Real.sin_add, pow_eq_pow_iff_of_ne_zero, exists_deriv_eq_zero, Complex.hasSum_arctan, exists_deriv_eq_slope, intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le, Real.hasSum_pow_div_log_of_abs_lt_one, taylor_mean_remainder_lagrange, deriv.lhopital_zero_nhds, bernoulli, taylorWithin, Complex.cos_add_sin_mul_I_pow, ProbabilityTheory.gaussianReal, hasSum_zeta_two, ProbabilityTheory.cond_eq_inv_mul_cond_mul, irrational_pi, MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable, Complex.exists_root, intermediate_value_Icc, Metric.tendsto_nhds_nhds, Complex.circleIntegral_sub_inv_smul_of_differentiable_on_off_countable, Nat.infinite_setOf_prime_and_eq_mod, TendstoUniformly, Quaternion, BooleanAlgebra, IsRiemannianManifold, RiemannHypothesis, Cardinal.not_countable_real, CommRing, MeasureTheory.IsProbabilityMeasure, Computable |
| Q1046291 | Topological group | IsTopologicalGroup, GroupTopology, ContinuousMonoidHom, continuous_of_continuousAt_one, ContinuousMulEquiv, instIsTopologicalAddGroupReal, Matrix.GeneralLinearGroup, Matrix.orthogonalGroup, LieGroup, PadicInt, ProfiniteGrp, Homeomorph.mulLeft, Homeomorph.inv, IsTopologicalGroup.rightUniformSpace, Subgroup.instIsTopologicalGroupSubtypeMem, OpenSubgroup.isClosed, Subgroup.topologicalClosure, Subgroup.is_normal_topologicalClosure, QuotientGroup.instTopologicalSpace, QuotientGroup.isOpenQuotientMap_mk, QuotientGroup.instIsTopologicalGroup, IsClosed.mul_left_of_isCompact, Subgroup.isClosed_of_discrete, ContinuousSMul, CauchySeq, UniformContinuous |
| Q179899 | Topological space | TopologicalSpace, IsClosed, IsClopen, IndiscreteTopology, DiscreteTopology, TopologicalSpace.ofClosed, TopologicalSpace.le_def, TopologicalSpace.instCompleteLattice, Continuous, Continuous.isOpen_preimage, Homeomorph, TopCat, FinTopCat, CofiniteTopology, Ordinal.instTopologicalSpace, sierpinskiSpace, instTopologicalSpaceSubtype, instTopologicalSpaceProd, instTopologicalSpaceQuotient, PseudoMetricSpace.toUniformSpace, Real.pseudoMetricSpace, TopologicalSpace.IsTopologicalBasis, IsTopologicalGroup, PrimeSpectrum.zariskiTopology, SpectralSpace, specializationPreorder, Filter.instTopologicalSpace |
| Q42989 | Topology | TopologicalSpace, Homeomorph, ContinuousMap.HomotopyEquiv, T2Space, IsOpen, IsClosed, IsClopen, TopologicalSpace.OpenNhds, Continuous, Metric.continuous_iff, ChartedSpace, IsCompact, IsConnected, MetricSpace, Metric.isOpen_iff, HomotopyGroup, subgroupIsFreeOfIsFree, CategoryTheory.GrothendieckTopology |
| Q12510 | Torus | UnitAddTorus |
| Q369377 | Total order | LinearOrder, extend_partialOrder, IsStrictTotalOrder, le_iff_lt_or_eq, asymm_of_isTrans_of_irrefl, Subtype.instLinearOrder, instLinearOrderEmpty, Ordinal.instLinearOrder, LinearOrder.lift, Pi.Lex.linearOrder, Real.linearOrder, IsStrictOrderedRing, ConditionallyCompleteLinearOrderedField.inducedOrderRingIso, IsChain, zorn_le, WellFoundedGT.monotone_chain_condition, IsNoetherianRing, RelSeries.length, LinearOrder.toLattice, DistribLattice, Finite.to_wellFoundedLT, monoEquivOfFin, StrictMono.orderIsoOfSurjective, Set.Ioo, OrderTopology, OrderTopology.t5Space, ConditionallyCompleteLinearOrder, compactSpace_of_completeLinearOrder, Sum.Lex.linearOrder, Sigma.Lex, Prod.Lex.instLinearOrder, Prod.instPartialOrder, Order.Preimage.instIsStrictWeakOrder, PartialOrder, IsOrderedMonoid |
| Q173091 | Transcendental number | Transcendental, isAlgebraic_iff_isIntegral, Transcendental.irrational, irrational_pi, transcendental_liouvilleNumber, Liouville, Liouville.transcendental, Algebraic.countable, Complex.exp_pi_mul_I, Cardinal.not_countable_real, AlgebraicIndependent, AlgebraicClosure.isAlgClosed, isAlgebraic_rat |
| Q2460595 | Transcendental number theory | Transcendental, AlgebraicIndependent, exists_pos_real_of_irrational_root, Algebraic.countable |
| Q840810 | Transfinite induction | Ordinal.induction, Ordinal.limitRecOn, Module.Basis.ofVectorSpace, WellFoundedLT.fix, IsWellFounded.fix |
| Q46303 | Trapezoid | trapezoidal_integral |
| Q272735 | Tree (graph theory) | SimpleGraph.isTree_iff_existsUnique_path, SimpleGraph.isAcyclic_iff_path_unique, SimpleGraph.isTree_iff_connected_and_card, SimpleGraph.IsAcyclic, SimpleGraph.IsTree, SimpleGraph.IsTree.isBipartite, SimpleGraph.Connected.exists_isTree_le, SimpleGraph.pathGraph, SimpleGraph.starGraph |
| Q19821 | Triangle | Affine.Triangle, EuclideanGeometry.angle_add_angle_add_angle_eq_pi, Affine.Simplex, Affine.Triangle.prod_div_one_sub_eq_one_of_mem_line_point_lineMap, AffineSubspace.perpBisector, Affine.Simplex.circumsphere, EuclideanGeometry.Sphere.thales_theorem, Affine.Simplex.altitude, Affine.Triangle.eq_orthocenter_of_forall_mem_altitude, Affine.Simplex.insphere, Affine.Simplex.exsphere, Affine.Simplex.ninePointCircle, Affine.Simplex.ninePointCircle_radius, Affine.Simplex.median, Affine.Simplex.eq_centroid_of_forall_mem_median, Affine.Simplex.point_vsub_centroid_eq_smul_vsub, EuclideanGeometry.exterior_angle_eq_angle_add_angle, EuclideanGeometry.law_cos, Similar, EuclideanGeometry.similar_of_angle_angle, EuclideanGeometry.similar_of_side_angle_side, similar_of_side_side, EuclideanGeometry.triangle_congruent_iff_dist_eq, EuclideanGeometry.side_angle_side, EuclideanGeometry.angle_side_angle, EuclideanGeometry.side_side_side, EuclideanGeometry.angle_angle_side, dist_triangle, AffineBasis.coord, Affine.Simplex.altitudeFoot, Affine.Simplex.inradius, Finset.centroid, EuclideanGeometry.angle, segment, Collinear |
| Q208216 | Triangle inequality | dist_triangle, norm_add_le, EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two, dist_le_range_sum_dist, sameRay_iff_norm_add, Real.norm_eq_abs, PiLp.norm_eq_sum, EuclideanSpace.norm_eq, norm_inner_eq_norm_iff, Real.Lp_add_le, Filter.Tendsto.cauchySeq, dist_eq_norm, abs_norm_sub_norm_le, lipschitzWith_one_norm, abs_dist_sub_le, parallelogram_law_with_norm, norm_inner_le_norm, MeasureTheory.Lp, InnerProductSpace, CauchySeq |
| Q93344 | Trigonometric functions | Real.sin, Real.sin_pi_div_two_sub, Real.sin_sq_add_cos_sq, Real.tan_eq_sin_div_cos, Real.sin_periodic, Real.cos_pi_div_four, Real.sin_eq_tsum, Complex.meromorphic_tan, Complex.tendsto_euler_sin_prod, Complex.exp_mul_I, Complex.sin, Complex.sin_eq, Real.sin_eq_zero_iff, Real.sin_add_pi, Real.cos_neg, Real.one_add_tan_sq_mul_cos_sq_eq_one, Complex.sin_add, Complex.cos_two_mul, Real.sin_eq_two_mul_tan_half_div_one_add_tan_half_sq, Real.two_mul_cos_mul_cos, Real.hasDerivAt_sin, Real.arcsin, EuclideanGeometry.sin_angle_div_dist_eq_sin_angle_div_dist, InnerProductGeometry.norm_sub_sq_eq_norm_sq_add_norm_sq_sub_two_mul_norm_mul_norm_mul_cos_angle |
| Q8084 | Trigonometry | Real.sin, Real.cos, Real.tan, Real.cos_pi_div_two_sub, Circle, Real.arctan, Complex.hasSum_sin, Complex.exp_mul_I, EuclideanGeometry.sin_angle_mul_dist_eq_sin_angle_mul_dist, EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_sub_two_mul_dist_mul_dist_mul_cos_angle, Real.sin_sq_add_cos_sq, Complex.sin |
| Q600590 | Tuple | Fin.cons, Fin.elim0, Prod, Complex.equivRealProd, funext_iff, Fintype.card_fun, PUnit |
| Q163310 | Turing machine | Turing.TM0.Machine, ComputablePred.halting_problem, Turing.TM0.Cfg |
| Q1056428 | Type theory | Nat.succ, List.Vector |
| Q741865 | Uniform continuity | UniformContinuous, Metric.uniformContinuous_iff, Metric.continuous_iff, UniformContinuous.continuous, TotallyBounded.image, CompactSpace.uniformContinuous_of_continuous, Continuous.uniformContinuous_of_tendsto_cocompact, IsCompact.uniformContinuousOn_of_continuous, LipschitzWith.uniformContinuous, Real.uniformContinuous_abs, UniformEquicontinuous.uniformContinuous, UniformContinuous.comp_cauchySeq, ContinuousLinearMap.uniformContinuous |
| Q1411887 | Uniform convergence | TendstoUniformly, Filter.Tendsto, TendstoUniformlyOn, UniformCauchySeqOn.tendstoUniformlyOn_of_tendsto, Metric.tendstoUniformlyOn_iff, TendstoLocallyUniformly, tendstoUniformlyOn_tsum, TendstoUniformly.tendstoLocallyUniformly, tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact, tendstoLocallyUniformly_iff_forall_isCompact, Monotone.tendstoUniformlyOn_of_forall_tendsto, Equicontinuous.tendsto_uniformFun_iff_pi, TendstoUniformlyOn.continuousOn, hasFDerivAt_of_tendstoUniformly, TendstoUniformlyOn.tendsto_intervalIntegral_of_continuousOn, TendstoLocallyUniformlyOn.differentiableOn, Complex.IsConservativeOn.isExactOn_ball, BoundedContinuousFunction.instCompleteSpace, MeasureTheory.Lp, MeasureTheory.tendstoUniformlyOn_of_ae_tendsto, BoundedContinuousFunction, ContinuousMap.compactOpen, UniformCauchySeqOn, BoundedContinuousFunction.norm_def, UniformOnFun, TendstoUniformly.uniformContinuous, MeasureTheory.TendstoInMeasure, UniformFun |
| Q727103 | Unitary matrix | Matrix.mem_unitaryGroup_iff, Matrix.mem_specialUnitaryGroup_iff, ContinuousLinearMap.inner_map_map_of_mem_unitary, isStarNormal_of_mem_unitary, Unitary.spectrum_subset_circle, Matrix.unitaryGroup, Matrix.specialUnitaryGroup |
| Q1673406 | Universal enveloping algebra | UniversalEnvelopingAlgebra, UniversalEnvelopingAlgebra.lift, UniversalEnvelopingAlgebra.ι, FreeLieAlgebra.universalEnvelopingEquivFreeAlgebra |
| Q175199 | Variance | ProbabilityTheory.variance, ProbabilityTheory.covariance_self, ProbabilityTheory.variance_eq_sub, ProbabilityTheory.variance_nonneg, ProbabilityTheory.ae_eq_integral_of_variance_eq_zero, ProbabilityTheory.integral_condVar_add_variance_condExp, ProbabilityTheory.variance_add_const, ProbabilityTheory.variance_const_mul, ProbabilityTheory.variance_add, ProbabilityTheory.variance_sum, ProbabilityTheory.IndepFun.covariance_eq_zero, ProbabilityTheory.IndepFun.variance_sum |
| Q658429 | Vector bundle | VectorBundle, Bundle.Trivial.vectorBundle, tangentBundleCore, FiberBundle, Bundle.Trivialization, Bundle.Trivial, VectorBundleCore.coordChange, FiberBundleCore.coordChange_comp, FiberBundleCore.fiberBundle, ContMDiffSection, VectorBundle.prod, Bundle.ContinuousLinearMap.vectorBundle, VectorBundle.pullback, Bundle.RiemannianBundle, ContMDiffVectorBundle |
| Q200802 | Vector calculus | crossProduct, triple_product_eq_det, MeasureTheory.integral_divergence_prod_Icc_of_hasFDerivAt_off_countable_of_le, HasFDerivAt, IsLocalExtr.fderiv_eq_zero, EuclideanSpace, TangentBundle |
| Q186247 | Vector field | TangentBundle, IsManifold, ContMDiffSection, gradient, Matrix.orthogonalGroup, MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable, IsMIntegralCurve, IsPicardLindelof.exists_eq_forall_mem_Icc_eq_picard, LipschitzWith, VectorField.mlieBracket, mfderiv, VectorField.mpullback_mlieBracket, Derivation |
| Q125977 | Vector space | Module, AddCommMonoid, SMul.smul, Finsupp.linearCombination, LinearIndependent, Submodule, Submodule.span, Module.Basis, Module.Basis.exists_basis, mk_eq_mk_of_basis, Module.Basis.repr, Prod.instModule, Pi.module, Algebra, LinearMap.ker, LinearMap, LinearEquiv, Module.Dual, FiniteDimensional.nonempty_linearEquiv_of_finrank_eq, LinearMap.toMatrix, LinearMap.isUnit_iff_isUnit_det, Module.End.HasEigenvector, LinearMap.charpoly, Module.End.eigenspace, Submodule.hasQuotient, ModuleCat.abelian, DirectSum, LinearMap.mk₂, TensorProduct, TensorProduct.lift, PosSMulStrictMono, NormedSpace, EuclideanSpace, Submodule.orthogonal, ContinuousSMul, CompleteSpace, polynomialFunctions_closure_eq_top, exists_extension_norm_eq, MeasureTheory.Lp, MeasureTheory.Lp.instCompleteSpace, InnerProductSpace, ContinuousMap.subalgebra_topologicalClosure_eq_top_of_separatesPoints, Polynomial, LieAlgebra, TensorAlgebra, ExteriorAlgebra, VectorBundle, TangentBundle, Module.Free, AddTorsor, AffineSubspace, Projectivization |
| Q1970172 | Von Neumann algebra | VonNeumannAlgebra, WStarAlgebra, IsStarProjection |
| Q37172 | Wave | fourierIntegral_gaussian |
| Q831390 | Wavelet | MeasureTheory.Lp |
| Q659746 | Well-order | IsWellOrder, WellOrder, WellFounded.has_min, SuccOrder.ofLinearWellFoundedLT, WellFoundedLT.conditionallyCompleteLinearOrderBot, isWellOrder_lt, Ordinal.type, exists_wellFoundedLT, WellFoundedLT.induction, Ordinal.type_nat_lt, wellFounded_iff_isEmpty_descending_chain, PrincipalSeg.ofElement, InitialSeg.isLowerSet_range, ZFSet.IsOrdinal, PrincipalSeg.irrefl, InitialSeg.total, InitialSeg.image_Iio, Ordinal, Preorder.topology, IsCofinal, Ordinal.type_fintype, Ordinal.limitRecOn |
| Q576728 | Winding number | FundamentalGroup |
| Q3573180 | Yuktibhāṣā | Real.hasSum_arctan, Real.tendsto_sum_pi_div_four, Real.pi_lt_d20, Real.hasSum_sin, Real.cos_add, taylor_mean_remainder_lagrange |
| Q191849 | Zermelo–Fraenkel set theory | ZFSet.ext, ZFSet.regularity, ZFSet.mem_irrefl, ZFSet.rank, ZFSet.sep, ZFSet.empty, ZFSet.mem_pair, ZFSet.sUnion, ZFSet.image, ZFSet.omega, ZFSet.subset_def, ZFSet.powerset, ZFSet.choice_mem, zorn_le |
| Q899731 | Zeros and poles | MeromorphicOn, MeromorphicAt.inv_iff, AnalyticOnNhd, meromorphicOrderAt, MeromorphicAt.eventually_eq_zero_or_eventually_ne_zero |
| Q290810 | Zorn's lemma | zorn_le, exists_extension_of_le_sublinear, AlgebraicClosure, exists_wellOrder, IsChain.exists_maxChain, PartialOrder, GE.ge, LinearOrder, Subtype.partialOrder, IsChain, IsMax, upperBounds, exists_maximal_of_chains_bounded, zorn_le_nonempty_Ici₀, Module.Basis.exists_basis, LinearIndependent, Ideal.exists_maximal, isCompact_univ_pi, ChainCompletePartialOrder.nonempty_fixedPoints_of_inflationary, Ultrafilter.exists_le, Classical.choice, Reflexive, Std.Antisymm, Transitive, Ideal, Ideal.IsMaximal, CompactSpace, Module.Basis, Ultrafilter, Directed, Preorder, IsWellOrder, Ordinal.limitRecOn, Order.IsSuccLimit, ChainCompletePartialOrder, CompletePartialOrder, InitialSeg, Order.succ, Ordinal, isCompact_generateFrom, Ideal.IsPrime, Submodule.span, ZFSet.isOrdinal_notMem_univ |
| Q8078429 | Étale cohomology | AlgebraicGeometry.Scheme.Etale, AlgebraicGeometry.Scheme.EllAdicCohomology, AlgebraicGeometry.Scheme.ellAdicSheaf |