| Q204 | 0 | zero_add, mul_zero, Nat.zero_le, Even.zero, Ideal.bot_prime, 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 |
| Q199 | 1 | Nat.succ, one_mul, one_pow, MulOneClass, IsUnit, Nat.factorial_one, Finset.prod_empty, unitInterval, 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.instance.Abelian, 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.imageFactorisation, 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, instCommGroupUnits, Subgroup.normal_of_isMulCommutative, Subgroup.toCommGroup, CommGroup.is_simple_iff_prime_card, forget₂AddCommGroupIsEquivalence, AddCommGroup.toIntModule, AddCommGroup.equiv_free_prod_directSum_zmod, AddMonoidHom.add, Module.rank, Module.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, Int.instIsAddCyclic, DivisibleBy, Monoid.IsTorsion, Monoid.IsTorsionFree, Submodule.instIsTorsionFree, AddCommGrpCat.instAbelian |
| 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 |
| Q32043 | Addition | HAdd.hAdd, add_comm, add_assoc, Nat.succ_eq_add_one, add_zero, Finset.sum, tsum, Cardinal.add_def, AddMonoid.nsmul_succ, Nat.add, Nat.add_assoc, Int.add, Rat.add, div_add_div_same, Rat.add_comm, CauSeq.add, Complex.add_re, AddCommGroup, Pi.instAdd, Matrix.instAdd, ZMod, Real.Angle, AddCommSemigroup, Finsupp.linearCombination, Ordinal.add, Cardinal.instCommSemiring, CategoryTheory.Limits.coprod, sub_eq_add_neg, Real.exp_add, Distrib, add_div, Cardinal.add_eq_max, add_max, Tropical, ProbabilityTheory.IndepFun |
| 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.MonoidalClosed.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.Monad.adjToMonadIso |
| Q1017106 | Adjoint representation | LieAlgebra.ad, LieDerivation.ad_ker_eq_center, LieAlgebra.ad_lie, LieAlgebra.ad_pow_lie, LieAlgebra.IsKilling.rootSystem |
| Q382520 | Affine geometry | AffineMap, AffineSpace, 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, AffineBasis.toMatrix_vecMul_coords, AffineSubspace.map, MvPolynomial.zeroLocus, MvPolynomial, MvPolynomial.vanishingIdeal_zeroLocus_eq_radical |
| 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, AlgHom, AlgEquiv, Subalgebra, Algebra.TensorProduct.leftAlgebra, Unitization, DualNumber, MonoidAlgebra, Polynomial.algebraOfAlgebra, ContinuousMap.algebra, IncidenceAlgebra, Module.End.instAlgebra, RingHom.toAlgebra, Algebra.instSubringCenter |
| 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, FiniteDimensional, Rat.numberField, CyclotomicField, Algebra.IsAlgebraic, Algebra.IsAlgebraic.of_finite, Polynomial.Monic, IsIntegral, isIntegral_algebraMap, GCDMonoid.toIsIntegrallyClosed, IsIntegral.add, NumberField.RingOfIntegers, IsDedekindDomain, Ideal.uniqueFactorizationMonoid, EuclideanDomain.to_principal_ideal_domain, NumberField.instFintypeClassGroup, NumberField.classNumber_eq_one_iff, NumberField.dedekindZeta, NumberField.tendsto_sub_one_mul_dedekindZeta_nhdsGT, Nat.infinite_setOf_prime_and_eq_mod, NumberField.RingOfIntegers.basis, PowerBasis, Field.exists_primitive_element, Algebra.lmul, Algebra.trace, Algebra.traceForm, NumberField.discr, Rat.AbsoluteValue.equiv_real_or_padic, padicNorm, 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, Ideal.ramificationIdx, NumberField.not_dvd_discr_iff_forall_liesOver, IsCyclotomicExtension.autEquivPow, absoluteGaloisGroup, IsGalois.intermediateFieldEquivSubgroup, BrauerGroup |
| 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, singularHomologyFunctor, HomologicalComplex.homology, IsManifold, Geometry.SimplicialComplex, 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 |
| Q8366 | Algorithm | 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, Complex.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, expSeries_radius_eq_top, differentiableOn_riemannZeta |
| Q134787 | Analytic geometry | polarCoord, EuclideanSpace.sphere_zero_eq, AffineMap.lineMap, EuclideanSpace.dist_eq, Matrix.dotProduct |
| 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 |
| Q11500 | Area | Real.volume_Icc_pi, MeasureTheory.measureReal_nonneg, MeasureTheory.measure_union_add_inter, MeasureTheory.measure_diff, EuclideanSpace.volume_ball_fin_two, MeasureTheory.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, div_add_div_same, 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, MulChar.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, treesOfNumNodesEq_card_eq_catalan, Real.instField, gcd_assoc, Set.inter_assoc, Function.comp_assoc, Category.assoc, Matrix.mul_assoc, max_assoc |
| Q755991 | Atiyah–Singer index theorem | IsManifold, ContMDiffVectorBundle |
| Q202785 | Average | Finset.expect |
| Q17736 | Axiom | FirstOrder.Language.Theory, ConditionallyCompleteLinearOrderedField.uniqueOrderRingIso, FirstOrder.Language.Theory.exists_elementaryEmbedding_card_eq |
| Q179692 | Axiom of choice | Classical.axiomOfChoice, Classical.nonempty_pi, Classical.em, Cardinal.linearOrder, Cardinal.mul_eq_self, Function.Surjective.hasRightInverse, Cardinal.exists_wellFoundedLT, IsChain.exists_maxChain, zorn_le, Order.IsOfFiniteCharacter.exists_maximal, Cardinal.sum_lt_prod, Basis.ofVectorSpace, Ideal.exists_maximal, Module.Projective.of_free, Module.Baer.injective, CategoryTheory.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 |
| 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 |
| 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, ContinuousLinearMap.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, Isometry.toRealAffineIsometryEquiv, fderiv |
| Q737851 | Banach–Tarski paradox | Equidecomp, FreeGroup, Equidecomp.trans |
| 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 |
| 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.Types.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.Types.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, 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 |
| Q4973304 | Boolean algebra (structure) | DistribLattice.booleanAlgebraOfComplemented, BooleanAlgebra.toBooleanRing, BooleanAlgebra, PUnit.instBooleanAlgebra, inf_eq_left, BooleanAlgebra.toBoundedOrder, compl_unique, OrderDual.instBooleanAlgebra, Bool.instBooleanAlgebra, Set.instBooleanAlgebra, TopologicalSpace.Clopens.instBooleanAlgebra, instBooleanAlgebraSubtypeIsIdempotentElem, BoundedLatticeHom, map_compl', OrderIso, 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 | AffineMap.lineMap, AffineMap.lineMap_apply_module, bernsteinPolynomial |
| 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, ContinuousLinearMap.instCStarAlgebra, 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, Cardinal.le_def, 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, 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 |
| Q22952648 | Cardinality of the continuum | Cardinal.continuum, Cardinal.mk_set_nat, Cardinal.eq, Cardinal.mk_Ioo_real, Cardinal.not_countable_real, Cardinal.cantor, Function.Embedding.schroeder_bernstein, Cardinal.mk_real, Cardinal.continuum_power_aleph0, Cardinal.beth, Cardinal.sum_lt_prod, Algebraic.cardinalMk_of_countable_of_charZero |
| Q62912 | Cartesian coordinate system | EuclideanSpace, EuclideanSpace.equiv, EuclideanSpace.dist_eq, IsometryEquiv, AffineEquiv.constVAdd, Orientation.rotation, LinearMap.toMatrix_comp, AffineMap, AffineIsometryEquiv, Matrix.transvection, Orientation, positiveOrientation, EuclideanSpace.basisFun, Complex.equivRealProd |
| Q719395 | Category (mathematics) | CategoryTheory.Category, CategoryTheory.Functor, Quiver.Hom, CategoryTheory.SmallCategory, CategoryTheory.LocallySmall, CategoryTheory.types, CategoryTheory.RelCat, CategoryTheory.Discrete, Preorder.smallCategory, Quiver.IsThin, CategoryTheory.SingleObj, CategoryTheory.Iso, CategoryTheory.Groupoid, FundamentalGroupoid, CategoryTheory.Paths, Preord, CategoryTheory.ConcreteCategory, GrpCat, Ab, CategoryTheory.Cat, CategoryTheory.Functor.category, CategoryTheory.Category.opposite, CategoryTheory.prod, CategoryTheory.Quotient, CategoryTheory.Over, CategoryTheory.Under, CategoryTheory.Localization, CategoryTheory.Mono, CategoryTheory.Epi, CategoryTheory.IsSplitEpi, CategoryTheory.IsSplitMono, CategoryTheory.IsIso, CategoryTheory.End, CategoryTheory.End.monoid, CategoryTheory.Aut, CategoryTheory.IsSplitEpi.epi, CategoryTheory.Preadditive, CategoryTheory.Abelian, AddCommGrpCat, CategoryTheory.EnrichedCategory, CategoryTheory.Limits.HasLimits, CategoryTheory.Limits.Types.hasLimitsOfSize, CategoryTheory.CartesianClosed |
| Q217413 | Category theory | CategoryTheory.Category, CategoryTheory.types, CategoryTheory.Mono, CategoryTheory.SplitEpi.epi, CategoryTheory.Functor, CategoryTheory.Functor.op, CategoryTheory.NatTrans, CategoryTheory.NatIso, 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, DifferentiableOn.contDiffOn, TendstoLocallyUniformlyOn.differentiableOn, 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, sq_sum_div_le_sum_sq_div, sum_mul_sq_le_sq_mul_sq, inner_mul_inner_self_le, norm_add_le, continuous_inner, InnerProductGeometry.angle, inner_le_Lp_mul_Lq |
| 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 |
| Q190391 | Central limit theorem | ProbabilityTheory.tendstoInDistribution_inv_sqrt_mul_sum_sub, ProbabilityTheory.strong_law_ae_real, ProbabilityTheory.tendsto_charFun_inv_sqrt_mul_pow, ProbabilityTheory.charFun_inv_sqrt_mul_sum |
| 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 |
| 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.TM2Computable |
| 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, QuadraticForm.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.equivProd, lipschitzGroup, pinGroup |
| Q104845546 | Closed graph theorem (functional analysis) | LinearMap.continuous_of_isClosed_graph, IsBoundedLinearMap.isLinearMap_and_continuous_iff_isBoundedLinearMap, 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 |
| 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.succ_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_symm, IsAntichain.sperner |
| Q727659 | Commutative algebra | IsNoetherianRing, Polynomial.isNoetherianRing, Ideal.IsPrimary, Submodule.isLasker, Submodule.IsMinimalPrimaryDecomposition.radical_eq_associatedPrimes, 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.instCommRing, 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, AlgebraicGeometry.instFiniteRingKrullDim, 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, IsLocalRing.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 |
| Q381892 | Compact space | IsCompact.exists_isMaxOn, CompactSpace, isCompact_iff_isClosed_bounded, IsCompact, tendsto_subseq_of_bounded, BoundedContinuousFunction.arzela_ascoli, CompactSpace.uniformContinuous_of_continuous, isCompact_Icc, isCompact_closedBall, isCompact_iff_compactSpace, lebesgue_number_lemma_of_metric, IsCompact.isBounded, CompleteLattice, ContinuousMap.evalRingHom, IsClosed.isCompact, IsCompact.union, IsCompact.image, isCompact_univ_pi, UniformSpace.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, Real.noncompactSpace, compactSpace_of_completeLinearOrder, isCompact_sphere, WeakDual.isCompact_closedBall, isCompact_cantorSet, spectrum.isCompact, MeasureTheory.IsTightMeasureSet.isCompact_closure, MeasureTheory.IsTightMeasureSet, PrimeSpectrum.compactSpace, WeakDual.CharacterSpace.instCompactSpace, ProfiniteGrp |
| 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, ContractingWith.fixedPoint, HasStrictFDerivAt.toOpenPartialHomeomorph, UniformSpace.Completion, Completion.extension_unique, AbstractCompletion.compareEquiv, Completion.instPseudoMetricSpace, Completion.coe_isometry, Real.equivCauchy, Padic, UniformSpace.Completion.instNormedSpace, UniformSpace.Completion.innerProductSpace, IsCompletelyMetrizableSpace, PolishSpace, IsTopologicalGroup.completeSpace_rightUniformSpace_iff_leftUniformSpace, Cauchy |
| Q193756 | Complex analysis | DifferentiableOn, deriv, DifferentiableOn.analyticOnNhd, MeromorphicOn, differentiableAt_complex_iff_differentiableAt_real, AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq, Conformal, ConformalAt, IsConformalMap, 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, RCLike.aeval_conj, starRingEnd, Complex.conj_eq_iff_im, Complex.norm_conj, star_involutive, Complex.exp_conj, Complex.conjAe, Matrix.conjTranspose, Quaternion.instStarRing, StarMul.star_mul |
| Q11567 | Complex number | Complex, Complex.re, Complex.instAdd, Complex.instMul, Complex.instField, Complex.conj, Complex.conj_conj, Complex.conj_eq_iff_real, Complex.norm_def, Complex.dist_eq, 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, Complex.exp, Complex.exp_mul_I, Complex.exp_pi_mul_I, Complex.log, Complex.log_im, Complex.cpow, Complex.sin, DifferentiableAt.hasDerivAt_of_isLinearMap_of_cauchyRiemann, AnalyticOnNhd.eqOn_of_preconnected_of_frequently_eq, MeromorphicAt, IsAlgebraic, GaussianInt, Module.End.exists_eigenvalue, Rat.AbsoluteValue.equiv_real_or_padic |
| Q328998 | Complex plane | Complex, Complex.equivRealProdAddHom, Complex.arg_mul_coe_angle, Complex.rotation, Complex.re, Complex.polarCoord, Complex.arg, Complex.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 | Turing.TM2ComputableInPolyTime, Turing.TM0.Machine |
| Q830340 | Computer algebra system | EuclideanDomain.gcd, MvPolynomial.schwartz_zippel_sup_sum, ZMod.chineseRemainder, Polynomial.derivative |
| Q1575634 | Concrete category | CategoryTheory.ConcreteCategory, CategoryTheory.forget, PartialFun, CategoryTheory.SingleObj, Preorder.smallCategory, CategoryTheory.RelCat, CategoryTheory.Cat |
| 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, SimplyConnectedSpace.nonempty_homeomorph_sphere_three, ContinuousMap.HomotopyEquiv.nonempty_homeomorph_sphere, 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, LocPathConnectedSpace.toLocallyConnectedSpace, pathConnectedSpace_iff_connectedSpace, IsConnected.closure, isOpen_connectedComponent, biUnion_connectedComponent_pathComponent_eq, Quotient.instConnectedSpace, Pi.connectedSpace, IsOpen.locallyConnectedSpace, ChartedSpace.locPathConnectedSpace, PreirreducibleSpace.preconnectedSpace, SimplyConnectedSpace.instPathConnectedSpace, ContractibleSpace.toPathConnectedSpace |
| Q338047 | Context-free grammar | ContextFreeGrammar, ContextFreeGrammar.language, Language.IsContextFree, Symbol.nonterminal, Symbol.terminal, ContextFreeRule, ContextFreeGrammar.initial, ContextFreeGrammar.Produces, ContextFreeGrammar.Derives |
| Q170058 | Continuous function | Continuous, ContinuousAt, ContinuousOn, Polynomial.continuous, continuous_of_discreteTopology, SeqContinuous, Metric.continuous_iff, oscillation_eq_zero, Continuous.comp, ContinuousAt.preimage_mem_nhds, intermediate_value_Icc, IsCompact.exists_isMinOn, Differentiable.continuous, ContDiff, ContinuousOn.intervalIntegrable, tendsto_pi_nhds, TendstoUniformly.continuous, ContinuousWithinAt, continuousAt_iff_continuous_left_right, LowerSemicontinuous, LinearMap.continuous_iff_isClosed_ker, UniformContinuous, UniformContinuous.continuous, HolderWith, LipschitzWith, continuous_iff_isClosed, continuous_iff_continuousAt, continuous_iff_seqContinuous, continuous_iff_image_closure_subset_closure_image, continuousAt_iff_ultrafilter, IsCompact.image, IsConnected.image, IsPathConnected.image, IsLindelof.image, IsSeparable.image, continuous_id_iff_le, IsOpenMap, Homeomorph, Continuous.homeoOfEquivCompactToT2, TopologicalSpace.coinduced, TopologicalSpace.induced, IsDenseInducing.extend, Continuous.ext_on, ScottContinuousOn |
| Q208416 | Continuum hypothesis | Cardinal.sum_lt_prod, Cardinal.eq, Cardinal.mkRat, Cardinal.aleph0_lt_continuum, Cardinal.aleph_one_le_iff, 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, 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, Convexity.ConvexSpace |
| 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.ModEq.cancel_left_div_gcd, IsCoprime.dvd_of_dvd_mul_right, IsCoprime.pow, Pairwise, IsCoprime, Ideal.isCoprime_iff_add, Ideal.quotientInfRingEquivPiQuotient |
| Q186290 | Correlation | ProbabilityTheory.IndepFun.covariance_eq_zero, ProbabilityTheory.HasGaussianLaw.indepFun_of_covariance_eq_zero |
| Q66707394 | Countable set | Set.Countable, Denumerable, Function.cantor_surjective, countable_iff_exists_injective, countable_iff_exists_surjective, Uncountable, Infinite, Equiv, Cardinal.eq, Cardinal.not_countable_real, Cardinal.mk_real, Set.Finite.countable, Set.countable_infinite_iff_nonempty_denumerable, Denumerable.prod, Algebraic.countable, Subtype.countable, Set.Countable.mono, Set.Countable.prod, Denumerable.int, Set.Countable.union, Set.countable_iUnion, denumerableList, Set.countable_setOf_finite_subset, Function.Injective.countable, Cardinal.cantor, IsWellOrder |
| 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 |
| 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 |
| 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 |
| 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 |
| Q161973 | Curve | Path, eVariationOn, HasUnitSpeedOn, LipschitzWith.locallyBoundedVariationOn, WeierstrassCurve.IsElliptic |
| Q245462 | Cyclic group | IsCyclic, intCyclicAddEquiv, IsCyclic.commGroup, isSimpleGroup_of_prime_card, Subgroup.zpowers, ZMod, Int.instIsAddCyclic, ZMod.instIsAddCyclic, ZMod.isUnit_iff_coprime, ZMod.instField, ZMod.isCyclic_units_iff, isCyclic_subgroup_units, rootsOfUnity, rootsOfUnity.isCyclic, instIsCyclicAlgEquiv, 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 |
| 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, 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, Basis.orientation_eq_iff_det_pos, MeasureTheory.integral_image_eq_integral_abs_det_fderiv_smul, LinearMap.det, Matrix.permanent, Algebra.norm |
| Q1058314 | Diffeomorphism | Diffeomorph, Diffeomorph.toHomeomorph, IsLocalDiffeomorph, IsImmersion |
| 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 | 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, RiemannianMetric, pathELength_comp_of_monotoneOn, EuclideanGeometry.law_cos |
| Q1058681 | Differential operator | gradient, ContinuousLinearMap.adjoint, MeasureTheory.L2.inner_def, LinearPMap.IsFormalAdjoint, LinearMap.IsSymmetric, deriv_add |
| 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 |
| 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, klDiv, SimpleGraph.dist, MetricSpace, Metric.hausdorffDist, TopologicalSpace.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 |
| Q1226939 | Division (mathematics) | Nat.div_add_mod, div_eq_mul_inv, add_div, Int.euclideanDomain, Rat.instField, Real.instField, Complex.inv_def, Polynomial.div, Finite.isField_of_domain, deriv_div |
| 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, Odd, 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 |
| Q181365 | Dot product | Matrix.dotProduct, InnerProductGeometry.cos_angle_mul_norm_mul_norm, Matrix.add_dotProduct, InnerProductSpace, EuclideanSpace.basisFun, EuclideanSpace.inner_eq_star_dotProduct, Matrix.smul_dotProduct, inner_eq_zero_iff, 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 |
| Q752487 | Dual space | Module.Dual, StrongDual, Module.Dual.eval, Basis.dualBasis, Basis.dualBasis_apply_self, Module.lift_rank_lt_rank_dual, Module.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, Module.dualAnnihilator_gc, Submodule.dualQuotEquivDualAnnihilator, Module.dualProdDualEquivDual, LinearMap.toContinuousLinearMap, ContinuousLinearMap.toNormedAddCommGroup, WeakDual, InnerProductSpace.toDual, RealRMK.integral_rieszMeasure, NormedSpace.inclusionInDoubleDual, NormedSpace.inclusionInDoubleDualLi |
| Q638328 | Dynamical system | Flow.orbit, Conservative.measure_mem_forall_ge_image_count_eq, Flow, Flow.fromIter, Flow.toFun, MeasureTheory.MeasurePreserving, nonempty_omegaLimit, Flow.toAddAction, IsInvariant |
| Q82435 | E (mathematical constant) | ProbabilityTheory.gaussianReal, Stirling.tendsto_stirlingSeq_sqrt_pi, NormedSpace.exp_eq_tsum_div, Real.hasDerivAt_exp, Real.add_one_le_exp, Complex.exp_mul_I, Complex.exp_pi_mul_I, Complex.cos_add_sin_mul_I_pow |
| 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, 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, Unitary.spectrum_subset_circle, Matrix.charpoly_transpose, LinearMap.IsSymmetric.hasEigenvalue_iSup_of_finiteDimensional, Matrix.spectrum_diagonal, Module.End.eigenspaces_iSupIndep, Module.End.eigenspace_mem_invtSubmodule, LieModule.weightSpace |
| Q211294 | Elementary algebra | pow_zero, 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 |
| 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 | 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 |
| 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.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, EuclideanSpace.dist_eq, and_not_self_iff, em |
| Q116980063 | Euclidean planes in three-dimensional space | parallelepiped |
| Q17295 | Euclidean space | EuclideanSpace, OrthonormalBasis.repr, InnerProductSpace, AddTorsor, Module.finrank, VAdd.vadd, vsub_vadd, AddGroup.toAddTorsor, 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.instCompleteSpace, 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.linearIsometryEquiv, Module.reflection, Metric.isOpen_iff, Metric.isCompact_iff_isClosed_bounded |
| 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 |
| Q852973 | Euler characteristic | HomologicalComplex.homologyEulerChar, IncidenceAlgebra.Mu.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.range_exp_mul_I, Complex.norm_mul_exp_arg_mul_I, Complex.log, Complex.cos_add_sin_mul_I_pow, Complex.two_cos, Complex.cos, Circle.exp, Complex.exp_eq_one_iff, Quaternion.exp_of_re_eq_zero, Complex.exp_two_pi_mul_I |
| 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 |
| Q190026 | Euler's totient function | Nat.totient, Nat.totient_mul, Nat.totient_eq_prod_factorization, Nat.totient_eq_mul_prod_factors, Nat.totient_prime_pow, Nat.sum_totient, ArithmeticFunction.moebius, Nat.ModEq.pow_totient |
| Q200125 | Expected value | MeasureTheory.integral, MeasureTheory.integral_finset, MeasureTheory.integral_tsum, MeasureTheory.integral_pdf_smul, MeasureTheory.HasPDF, MeasureTheory.integral_eq_lintegral_pos_part_sub_lintegral_neg_part, MeasureTheory.lintegral_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, MeasureTheory.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, Complex.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 | Real.hasDerivAt_exp, Real.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_one, Complex.exp, Complex.cpow_def_of_ne_zero, Complex.exp_mul_I, Complex.abs_mul_exp_arg_mul_I, Complex.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, Matrix.pow_eq, iteratedDeriv, Field, GaloisField, add_pow_char, frobenius, Set.prod, Pi, Equiv.curry, Set.powerset, Cardinal.power_def, CategoryTheory.exp.adjunction, CategoryTheory.CartesianClosed, hyperoperation, Function.comp, Function.iterate, Function.invFun |
| Q1196652 | Exterior algebra | ExteriorAlgebra, exteriorPower, ExteriorAlgebra.gradedAlgebra, ExteriorAlgebra.lift, ExteriorAlgebra.ιMulti, ExteriorAlgebra.ι_sq_zero, ExteriorAlgebra.ι_add_mul_swap, AlternatingMap.map_perm, Module.Basis.exteriorPower, exteriorPower.finrank_eq, ExteriorAlgebra.instDecompositionExteriorPower, 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 |
| 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, fermatLastTheoremThree |
| 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, FiberBundleCore.coordChange_comp |
| Q23835349 | Fibonacci sequence | Nat.fib, Nat.fib_add_two, Int.fib, Real.coe_fib_eq, tendsto_fib_succ_div_fib_atTop, Real.goldenRatio_mul_fib_succ_add_fib, 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_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, DivisionRing.toGroupWithZero, isCyclic_of_subgroup_isDomain, CharP, CharP.char_is_prime_or_zero, frobenius, Subfield, RingHom, RingHom.injective, FiniteField, FiniteField.card', GaloisField.algEquivGaloisFieldOfFintype, CommRing, FractionRing, IsFractionRing.toField, IsLocalRing.ResidueField, PrincipalIdealRing.isMaximal_of_irreducible, IntermediateField.adjoin, IntermediateField.instSup, 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, IsTopologicalDivisionRing, Differential, IsGalois, Field.exists_primitive_element, AlgEquiv, IsGalois.intermediateFieldEquivSubgroup, not_solvable_by_rad, IsAlgClosed.equivOfTranscendenceBasis, FirstOrder.Language.ElementarilyEquivalent, FirstOrder.Language.Ultraproduct, Field.absoluteGaloisGroup, div_mul_cancel₀, AlgebraicGeometry.Scheme.functionField, NumberField, CyclotomicField, Rat.AbsoluteValue.equiv_real_or_padic, DivisionRing, littleWedderburn |
| Q577835 | Field extension | Algebra, Complex.instAlgebra, Subfield, SubfieldClass, Rat.instAlgebraReal, charP_of_injective_ringHom, IntermediateField, Module.finrank, FiniteDimensional, Module.finrank_mul_finrank, IntermediateField.adjoin, Field.exists_primitive_element, RingHom.injective, Zsqrtd, NumberField, AdjoinRoot, Polynomial.SplittingField, GaloisField, RatFunc, IsAlgebraic, IntermediateField.adjoin.finiteDimensional, algebraicClosure, Algebra.IsAlgebraic, AlgebraicClosure, AlgebraicIndependent, Normal, Algebra.IsSeparable, IsGalois.intermediateFieldEquivSubgroup, Algebra.IsCentral, TensorProduct.instAlgebra |
| Q203066 | Finitary relation | Relator.LeftTotal, Relator.LeftUnique, SetRel, Eq, Dvd.dvd, Membership.mem |
| Q2068418 | Finite difference | fwdDiff, fwdDiff_aux.fwdDiffₗ, hasDerivAt_iff_tendsto_slope, hasDerivAt_iff_tendsto_slope_zero, Polynomial.fwdDiff_iter_degree_eq_factorial, shift_eq_sum_fwdDiff_iter, hasSum_mahler, fwdDiff_aux.shiftₗ, fwdDiff_const, fwdDiff_smul, IncidenceAlgebra.mu |
| Q603880 | Finite field | FiniteField, 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, PerfectRing.ofFiniteOfIsReduced, Irreducible, Polynomial.uniqueFactorizationMonoid, AlgebraicClosure, littleWedderburn |
| 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 |
| 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 |
| 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.fourier_inversion, VectorFourier.fourierIntegral, MeasureTheory.Lp.fourierTransformₗᵢ, hasDerivAt_exp, Real.fourier_mul_convolution_eq, Real.fourierIntegral, Real.fourierIntegralInv, AddCircle.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, hasSum_fourier_series_L2, hasSum_fourier_series_of_summable |
| Q6520159 | Fourier transform | Real.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, MeasureTheory.charFun |
| Q81392 | Fractal | MeasureTheory.dimH, NowhereDifferentiable.exists_uniformContinuous_and_not_differentiableAt, cantorSet |
| Q1412452 | Fractal dimension | MeasureTheory.dimH |
| Q1149022 | Fubini's theorem | MeasureTheory.integral_prod, MeasureTheory.lintegral_prod, Summable.tsum_prod, MeasureTheory.Measure.prod, ENNReal.tsum_comm, MeasureTheory.integral_prod_mul, integral_gaussian |
| Q11348 | Function (mathematics) | Function.graph, Set.range, PFun, Rel, PFun.Dom, Nat.Partrec, Computability.halting_problem, Int.mul, Set.prod, Function.update, Polynomial, RatFunc, Function.Bijective, HasStrictFDerivAt.implicitFunction, Real.exp, HasFPowerSeriesAt, Nat.factorial, isEmptyElim, 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, Function.extend, Pi.instAdd, Real.log, Monotone, StrictMonoOn.orderIso, ContMDiffSection |
| 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 |
| Q864475 | Functor | CategoryTheory.Functor, CategoryTheory.Functor.op, CategoryTheory.prod, CategoryTheory.Functor.map_isIso, CategoryTheory.Functor.comp, CategoryTheory.SingleObj, TopCat.Presheaf, CategoryTheory.Functor.const, CategoryTheory.Functor.id, CategoryTheory.Functor.diag, CategoryTheory.Limits.lim, CategoryTheory.MonoidalCategory.tensor, CategoryTheory.forget, MonCat.free, CategoryTheory.Functor.hom, CategoryTheory.Functor.IsRepresentable, CategoryTheory.Functor.category |
| Q662830 | Fundamental group | FundamentalGroup, LoopSpace, Path.Homotopy, Path.Homotopic.equivalence, Path.trans, Path.Homotopic.Quotient.trans, FundamentalGroup.instGroup, 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 |
| Q44455 | Game theory | Sion.exists_isSaddlePointOn |
| Q117806 | Gamma distribution | ProbabilityTheory.gammaMeasure, ProbabilityTheory.gammaPDFReal, ProbabilityTheory.expMeasure |
| Q190573 | Gamma function | Complex.GammaIntegral, 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, Meromorphic.Gamma, 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 |
| Q2658 | Gaussian elimination | Matrix.det_updateRow_smul |
| 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, 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, isCompact_Icc, 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, 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, SeparableSpace, LindelofSpace, SigmaCompactSpace, FirstCountableTopology.frechetUrysohnSpace, SecondCountableTopology.to_firstCountableTopology, IsSigmaCompact.isLindelof, UniformSpace.firstCountableTopology, MetricSpace, EMetric.instParacompactSpace, metrizableSpace_of_t3_secondCountable, dense_sInter_of_isOpen, IsOpen.baireSpace, TopologicalSpace.MetrizableSpace |
| Q109744257 | Generalized hypergeometric function | NormedSpace.exp_eq_tsum, ascPochhammer, ordinaryHypergeometric |
| 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, Int.instAddCommGroup, FreeGroup, Monoid.CoprodI, Equiv.Perm, CoxeterSystem |
| 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 |
| 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 | 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 |
| 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, SimpleGraph.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, Quiver, Graph, SimpleGraph.Coloring, SimpleGraph.isTuranMaximal_iff_nonempty_iso_turanGraph, SimpleGraph.szemeredi_regularity, SimpleGraph.IsTree, SimpleGraph.incMatrix, SimpleGraph.adjMatrix, SimpleGraph.degMatrix, SimpleGraph.lapMatrix |
| 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, gcd_mul_lcm, Nat.totient_gcd_mul_totient_mul, GCDMonoid, UniqueFactorizationMonoid.toGCDMonoid, EuclideanDomain.gcd, span_gcd |
| Q83478 | Group (mathematics) | Group, Int.instCommGroup, 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 |
| Q288465 | Group action | MulAction, Representation, Equiv.Perm.applyMulAction, FaithfulSMul, MulAction.IsPretransitive, MulAction.IsMultiplyPretransitive, Equiv.Perm.isMultiplyPretransitive, MulAction.IsPreprimitive, ProperlyDiscontinuousSMul, ContinuousSMul, ProperSMul, IsSemisimpleRepresentation, MulAction.orbit, MulAction.orbitRel, MulAction.pretransitive_iff_subsingleton_quotient, MulAction.orbitRel.Quotient, MulAction.IsInvariantBlock, MulAction.IsFixedBlock.orbit, MulAction.fixedPoints, 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, CategoryTheory.Action, AlgEquiv.applyMulSemiringAction, Flow, Set.mulAction, CategoryTheory.ActionCategory, MulActionHom, CategoryTheory.actionAsFunctor |
| Q1055807 | Group representation | Action.ρAut, Representation, Action.IsContinuous, MonoidHom.ker, Representation.IntertwiningMap, Representation.Equiv, Subrepresentation, Representation.IsIrreducible, Representation.IsSemisimpleRepresentation, MulAction, MulAction.bijective, Action.functorCategoryEquivalence, Rep |
| Q1451046 | Gödel numbering | Nat.factorization_prod_pow_eq_self, Primrec.nat_strong_rec |
| Q200787 | Gödel's incompleteness theorems | FirstOrder.Language.Theory.IsComplete, FirstOrder.Field.ACF_isComplete, Nat.Partrec.Code.halting_problem |
| Q1162676 | Haar measure | borel, measurable_const_mul, MeasureTheory.Measure.IsMulLeftInvariant, MeasureTheory.Measure.IsMulRightInvariant, MeasureTheory.Measure.haarMeasure_unique, MeasureTheory.Measure.IsHaarMeasure, MeasureTheory.measure_ne_zero_iff_nonempty_of_isMulLeftInvariant, Real.isAddHaarMeasure_volume, MeasureTheory.Measure.haar.index, MeasureTheory.Measure.IsMulRightInvariant.inv, MeasureTheory.modularCharacterFun, MeasureTheory.integral, MeasureTheory.integral_mul_left_eq_self |
| 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, InnerProductSpace.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, t2Space_of_metrizableSpace, CofiniteTopology.instT1Space, PseudoMetrizableSpace.regularSpace, Prod.t2Space, T2Space.t1Space, R1Space.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 |
| Q82828 | Hexadecimal | Nat.digits_add_two_add_one |
| Q1617044 | Heyting algebra | HeytingAlgebra, GeneralizedHeytingAlgebra.toDistribLattice, BooleanAlgebra.toBiheytingAlgebra, inf_compl_self, TopologicalSpace.Opens.instFrame, HeytingAlgebra.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.abs, Complex.innerProductSpace, inner_conj_symm, inner_add_left, inner_self_eq_zero, inner_add_right, InnerProductSpace.Core.toNormedAddCommGroup, inner_mul_le_norm_mul_norm, summable_of_summable_norm, InnerProductSpace.toNormedSpace, Submodule.instInnerProductSpace, lp, lp.instInnerProductSpace, lp.instCompleteSpace, MeasureTheory.Lp, MeasureTheory.L2.innerProductSpace, MeasureTheory.Lp.instCompleteSpace, TemperedDistribution.MemSobolev, 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.instCStarAlgebra, IsSelfAdjoint, CFC.sqrt, unitary, IsCompactOperator, LinearPMap, LinearPMap.IsClosable, LinearPMap.adjoint, LinearMap.IsSymmetric, WithLp.prod, IsHilbertSum, HilbertBasis, Orthonormal.orthonormalBasis_of_dense_span, 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 |
| 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, 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 | norm_add_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two, Nat.Perfect, quadratic_eq_zero_iff, EuclideanGeometry.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, LucasLehmer.lucas_lehmer_sufficiency |
| Q5870804 | History of the function concept | Differentiable, Continuous, BooleanRing, Classical.epsilon, Partrec, halting_problem, ZFSet.sep, ZFSet.pair |
| 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_iff_preservesEpimorphisms_coyoneda_obj, TensorProduct.lift.equiv |
| Q202906 | Homeomorphism | Homeomorph, IsHomeomorph, Homeomorph.mulLeft, Homeomorph.isOpenMap |
| Q579978 | Homological algebra | ChainComplex, HomologicalComplex.d, HomologicalComplex.homology, HomologicalComplex.Acyclic, 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, singularHomologyFunctor, HomologicalComplex.Hom, HomologicalComplex.QuasiIso, HomologicalComplex.homologyFunctor, CategoryTheory.ShortComplex.ShortExact.δ |
| 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, 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, HomotopyGroup, 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 |
| Q837414 | Hypercomplex number | CliffordAlgebra, CliffordAlgebraComplex.equiv, Algebra.TensorProduct.instAlgebra |
| Q731894 | Hölder's inequality | ENNReal.lintegral_mul_le_Lp_mul_Lq, ENNReal.HolderConjugate, MeasureTheory.essSup, 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, MemLp.mono_exponent, eLpNorm_le_eLpNorm_mul_eLpNorm_of_nnnorm, MeasureTheory.eLpNorm_le_eLpNorm_of_exponent_le |
| Q321119 | Identity function | id, Function.bijective_id, Function.comp_id, Function.End, CategoryTheory.CategoryStruct.id, LinearMap.id, LinearMap.toMatrix_id, isometry_id, continuous_id |
| 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.PosDef.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_sq, InnerProductGeometry.angle, re_inner_eq_norm_add_mul_self_sub_norm_sub_mul_self_div_four, InnerProductSpace.rclikeToReal, OrthonormalBasis, HilbertBasis, HilbertBasis.repr, fourierBasis, ContinuousLinearMap, LinearMap.IsSymmetric, LinearIsometry, Isometric.toAffineIsometryEquiv, LinearIsometryEquiv, LinearMap.IsSymmetric.diagonalization, QuadraticForm.sigPos_eq_of_basis |
| 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, curveIntegral, 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, MeasureTheory.lintegral_mul_le_Lp_mul_Lq, MeasureTheory.lintegral_Lp_add_le, intervalIntegral.integral_symm, intervalIntegral.integral_add_adjacent_intervals, intervalIntegral.integral_hasDerivAt_right, MeasureTheory.AECover.integral_tendsto_of_countably_generated, MeasureTheory.integral_prod, trapezoidal_integral |
| Q187631 | Interpolation | AffineMap.lineMap, AffineMap.lineMap_apply_ring, Lagrange.interpolate, Lagrange.eq_interpolate_iff |
| Q185148 | Interval (mathematics) | Set.Icc, unitInterval, Set.OrdConnected, 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, Metric.continuous_iff, intermediate_value_Icc, OrderTopology.completelyNormalSpace, BoxIntegral.Box, Set.ordConnectedComponent |
| 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 |
| Q1855669 | Invariant theory | MvPolynomial.esymmAlgHom_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 |
| Q242188 | Invertible matrix | Invertible, Matrix.inv, Matrix.inv_def, Matrix.invOf_fromBlocks₂₂_eq, Matrix.add_mul_mul_inv_eq_sub, Matrix.det_one_add_mul_comm, Matrix.isUnit_iff_isUnit_det, Matrix.nonsing_inv_apply, Matrix.mul_eq_one_comm, Matrix.GeneralLinearGroup |
| Q189112 | Isomorphism | CategoryTheory.IsIsomorphic, CategoryTheory.Aut, Isometry, Homeomorph, Diffeomorph, Equiv.Perm, ZMod.chineseRemainder, RelIso, OrderIso, SimpleGraph.Iso, LinearIsometryEquiv, CategoryTheory.Iso, CategoryTheory.isIsomorphicSetoid, 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 |
| Q838495 | Jordan normal form | Module.End.genEigenspace, 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 |
| 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, DihedralGroup.instIsKleinFour, IsAddKleinFour.instZModProd, alternatingGroup.kleinFour |
| 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 |
| 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 |
| Q199691 | Laplace transform | ProbabilityTheory.mgf |
| Q339444 | Laplace's equation | HarmonicAt, HarmonicOnNhd.add, HarmonicContOnCl.circleAverage_poissonKernel_smul, AnalyticAt.harmonicAt_re, HarmonicAt.analyticAt, HarmonicOnNhd.circleAverage_eq |
| 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 |
| 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, lcm_zero_right, Finset.lcm, dvd_def, GCDMonoid.lcm, 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, MeasureTheory.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, 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, MeasureTheory.measure_zero_of_dimH_lt, BoxIntegral.Box, MeasureTheory.Measure.haarMeasure, MeasureTheory.hausdorffMeasure_pi_real |
| Q664495 | Lie algebra | LieAlgebra, LieAlgebra.ofAssociativeAlgebra, Cross.lieRing, LieRing.ofAssociativeRing, LieRing, lie_skew, leibniz_lie, LieSubalgebra.lieSpan, IsLieAbelian, LieRing.of_associative_ring_bracket, lieEquivMatrix', LieSubalgebra, LieIdeal, LieHom, LieEquiv, LieHom.quotKerEquivRange, LieSubalgebra.normalizer, instLieRing, LieAlgebra.SemiDirectSum, Derivation, Derivation.instLieAlgebra, LieDerivation.inner, LieDerivation.IsKilling.exists_eq_ad, LieAlgebra.SpecialLinear.sl, LieAlgebra.Orthogonal.so, LieAlgebra.Symplectic.sp, skewAdjointMatricesLieSubalgebra, 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 |
| Q622679 | Lie group | LieGroup, Matrix.GeneralLinearGroup, Matrix.specialOrthogonalGroup, Matrix.SpecialLinearGroup, Matrix.unitaryGroup, Matrix.orthogonalGroup, Matrix.specialUnitaryGroup, Matrix.symplecticGroup, GroupLieAlgebra, NormedSpace.exp |
| 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, Hyperreal.stdPart, Hyperreal.stdPart_of_tendsto, omegaLimit, HasSum, hasSum_zeta_two, Summable, FormalMultilinearSeries.radius, ContinuousAt, 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 |
| 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, Filter.limsup_add_le, Filter.le_liminf_add, Filter.limsup_mul_le, oscillation, Filter.liminf, Filter.limsup_compl, omegaLimit, Filter.limsSup, Filter.limsInf, Filter.atTop |
| 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.prod, 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 |
| Q82571 | Linear algebra | Module, AddCommGroup, LinearMap, Module.End, LinearEquiv, Submodule, LinearMap.range, Submodule.span, LinearIndependent, Basis, Basis.extend, mk_eq_mk_of_basis, FiniteDimensional.nonempty_linearEquiv_iff_finrank_eq, FiniteDimensional, Submodule.finrank_le, Submodule.finrank_sup_add_finrank_inf_eq, Basis.equivFun, 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, Basis.dualBasis, Module.Dual.eval, Module.evalEquiv, LinearMap.dualMap, LinearMap.toMatrix_transpose, InnerProductSpace, norm_eq_sqrt_re_inner, norm_inner_le_norm, OrthonormalBasis, gramSchmidtOrthonormalBasis, Matrix.conjTranspose, IsStarNormal, Module.Free, Submodule.basisOfPid, Module.tautologicalRelations, NormedSpace |
| Q484637 | Linear equation | AffineMap |
| Q207643 | Linear map | LinearMap, IsLinearMap, map_sum, LinearMap.map_zero, Module.Dual, LinearMap.lsmul, LinearMap.instZero, LinearMap.id, Matrix.toLin', LinearIsometry, Polynomial.derivative, LinearMap.toMatrix, LinearMap.smulRight, LinearMap.map_add, LinearMap.map_smul, LinearEquiv, Basis.constr, exists_extension_of_le_sublinear, Matrix.planeConformalMatrix, IsConformalMap, LinearMap.comp, LinearEquiv.symm, LinearMap.instAdd, LinearMap.instSMul, LinearMap.instModule, Module.End.instSemiring, LinearMap.GeneralLinearGroup, LinearMap.toMatrixAlgEquiv, LinearMap.ker, LinearMap.finrank_range_add_finrank_ker, LinearMap.rank, Submodule.Quotient, LinearMap.ker_eq_bot, LinearMap.range_eq_top, IsNilpotent, basis_toMatrix_mul_linearMap_toMatrix_mul_basis_toMatrix, LinearMap.continuous_iff_isBounded |
| Q202843 | Linear programming | IsMinOn.of_isLocalMin_of_convex_univ |
| 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 |
| 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_log, Real.deriv_log, logDeriv, integral_log, Real.log_rpow, harmonic, Real.tendsto_harmonic_sub_log, Complex.hasSum_taylorSeries_log, Complex.arg, Complex.exp_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, analyticAt_sigmoid |
| Q305936 | Lp space | EuclideanSpace.norm_eq, PiLp.norm_eq_sum, PiLp.norm_eq_ciSup, PiLp.instNormedAddCommGroup, PiLp.completeSpace, PiLp.norm_eq_card, 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.instSeminormedAddCommGroup, 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, MeasureTheory.ContinuousMap.toLp_denseRange, MeasureTheory.BoundedContinuousFunction.toLp_denseRange, MeasureTheory.mul_meas_ge_le_pow_eLpNorm |
| 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₁ |
| Q192089 | Magic square | 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.martingale_condExp, MeasureTheory.Submartingale, MeasureTheory.Supermartingale, MeasureTheory.martingale_iff, MeasureTheory.IsStoppingTime, MeasureTheory.submartingale_iff_expected_stoppedValue_mono |
| Q7754 | Mathematical analysis | MetricSpace, dist_nonneg, Stream'.Seq, Filter.Tendsto, ContinuousAt, MeasureTheory.Measure, Real.volume_Ioo |
| Q178377 | Mathematical induction | Nat.rec, Nat.le_induction, WellFounded.induction, Finset.sum_range_id, Nat.strong_induction_on, Nat.exists_prime_and_dvd |
| 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 | DFA |
| 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 |
| 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 |
| Q44337 | Matrix (mathematics) | Matrix, Matrix.isUnit_iff_isUnit_det, Matrix.add, Matrix.addCommMonoid, Matrix.smul, Matrix.transpose, Matrix.transpose_add, Matrix.mul, Matrix.mul_assoc, Matrix.submatrix, Matrix.toLin', LinearMap.toMatrix_comp, Matrix.rank, LinearMap.finrank_range_add_finrank_ker, Matrix.instRing, Matrix.one, Matrix.IsHermitian, Matrix.IsHermitian.spectral_theorem, Matrix.PosDef, Matrix.IsHermitian.posDef_iff_eigenvalues_pos, Matrix.toBilin', Matrix.orthogonalGroup, Matrix.specialOrthogonalGroup, Matrix.trace, Matrix.trace_mul_comm, Matrix.trace_transpose, Matrix.det, Matrix.det_fin_two, Matrix.det_mul, Matrix.det_succ_row_zero, Matrix.cramer, Module.End.HasEigenvalue, Matrix.charpoly, Matrix.aeval_self_charpoly, Matrix.fromBlocks, LinearMap.toMatrix, Matrix.GeneralLinearGroup, Matrix.SpecialLinearGroup, Matrix.det_isEmpty, Semiring, Matrix.semiring, Matrix.rowStochastic, SimpleGraph.adjMatrix, HasStrictFDerivAt.implicitFunction |
| Q1049914 | Matrix multiplication | Matrix.instHMul, Matrix.mul_apply, Matrix.mulVec, Matrix.vecMul, Matrix.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 |
| Q845060 | Maximum and minimum | IsMaxOn, IsLocalMax, IsCompact.exists_isMaxOn, IsLocalExtr.deriv_eq_zero, IsLocalExtr.fderiv_eq_zero, Maximal, IsLUB, IsLeast, IsGreatest, IsLeast.unique, Set.Finite.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 |
| Q226995 | Median | ConvexOn.map_integral_le |
| Q180953 | Metric space | MetricSpace, eq_of_dist_eq_zero, dist_pos, dist_comm, dist_triangle, Real.metricSpace, EuclideanSpace.dist_eq, PiLp.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, Bornology.IsBounded, Metric.diam, TotallyBounded, TotallyBounded.isBounded, Metric.isCompact_iff_totallyBounded_isComplete, 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, NormedSpace, LinearMap.continuous_of_bound, IsManifold, BoundedContinuousFunction, BoundedContinuousFunction.instCompleteSpace, Metric.infDist, Metric.infDist_zero_of_mem_closure, Metric.continuous_infDist_pt, Metric.hausdorffEDist, Metric.NonemptyCompacts.metricSpace, GromovHausdorff.GHSpace, Prod.metricSpaceMax, PiNat, EMetricSpace, PseudoMetricSpace |
| Q757269 | Metric tensor | Bundle.RiemannianMetric, IsRiemannianManifold, Continuous.inner_bundle, Bundle.RiemannianMetric.symm, norm_tangentSpace_vectorSpace, Bundle.RiemannianMetric.inner, Bundle.ContMDiffRiemannianMetric, Bundle.RiemannianMetric.pos, IsImmersion, mfderiv, IsContinuousRiemannianBundle, 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 |
| 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, DivInvMonoid.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, 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, Grp, 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.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.isMultiplicative_moebius, ArithmeticFunction.moebius_mul_coe_zeta, 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 |
| 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, Cardinal.le_def, Stream'.Seq, Ordinal.type, Ordinal.type_nat_lt, PNat, Nat.digits, Nat.succ, Nat.rec, PSet.ofNat, 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, Nat.instIsStrictOrderedRing, Nat.find, Nat.div_add_mod, Nat.div, Nat.div_mod_unique, 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.instLinearOrder, 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, mul_pos_iff, div_pos_of_neg_of_neg, div_pos_iff, neg_add_cancel, neg_neg, abs, Int.instCommRing, Int.instLinearOrder, neg_eq_of_add_eq_zero_left |
| Q374195 | Newton's method | hensels_lemma |
| 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 | Circle, DualNumber |
| 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 |
| 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 |
| Q215206 | NP-completeness | 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, Nat.Prime, Nat.exists_infinite_primes, 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, GaussianInt, Complex.isAlgClosed, Even, odd_iff_exists_bit1, Even.mul_right, mersenne, Nat.instUniqueFactorizationMonoid, IsAlgebraic, IsIntegral, Padic, Quaternion, Ordinal, 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, dedekindZeta, IsAlgebraic, NumberField, IsAbelianGalois, Real.infinite_rat_abs_sub_lt_one_div_den_sq_of_irrational, Transcendental |
| 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 |
| 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.zero_le, Order.succ, Order.IsSuccLimit, Ordinal.isSuccLimit_iff, 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, Ordinal.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 |
| 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, 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, Matrix.vecMulVecBilin, Matrix.rank_vecMulVec_le, TensorProduct.tmul, InnerProductSpace.rankOne, Matrix.det_vecMulVec |
| Q746242 | P versus NP problem | ComputablePred.halting_problem |
| Q48297 | Parabola | AffineMap |
| Q1413083 | Parameter | Real.logb, Nat.descFactorial, circleMap, ProbabilityTheory.poissonPMF, ProbabilityTheory.gaussianReal |
| 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 |
| Q271977 | Partial differential equation | InnerProductSpace.HarmonicAt, InnerProductSpace.instLaplacian |
| Q1756942 | Partial function | PFun, PFun.Dom, Nat.Partrec, partialFunEquivPointed |
| 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 |
| Q1187620 | Perfect graph | SimpleGraph.IsClique, SimpleGraph.cliqueNum, SimpleGraph.Coloring, SimpleGraph.chromaticNumber, SimpleGraph.cliqueNum_le_chromaticNumber, PartialOrder, IncompRel, IsChain, IsAntichain |
| Q170043 | Perfect number | Nat.Perfect, 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, PeriodPair.weierstrassP_add_coe, Function.Periodic.not_injective, Function.Periodic.intervalIntegral_add_eq, Function.Periodic.const_mul, Function.Periodic.add, Function.Antiperiodic, Function.Antiperiodic.periodic, Function.Periodic.lift |
| Q161519 | Permutation | Fintype.card_perm, Equiv.Perm, Equiv.permGroup, Equiv.Perm.one_def, Equiv.Perm.cycleFactorsFinset_noncommProd, Equiv.Perm.IsCycle, Function.IsFixedPt, derangements, Equiv.swap, Equiv.Perm.Disjoint.commute, Equiv.Perm.formPerm_reverse, Equiv.Perm.mul_apply, Equiv.trans, Fintype.card_embedding_eq, descPochhammer, Finset.powersetCard, Finset.card_powersetCard, Nat.choose, Fintype.card_pi_const, Equiv.Perm.cycleType, Equiv.Perm.card_of_cycleType, IsConj, Equiv.Perm.isConj_iff_cycleType_eq, orderOf, Equiv.Perm.lcm_cycleType, Equiv.Perm.truncSwapFactors, Equiv.Perm.sign, Matrix.det_permutation, Equiv.Perm.permMatrix, Matrix.permMatrixHom |
| 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, buffon_short, EuclideanSpace.volume_ball_fin_two, EuclideanSpace.volume_ball_fin_three, integral_sqrt_one_sub_sq, Real.sin_periodic, Real.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 |
| Q530152 | Picard–Lindelöf theorem | IsPicardLindelof.exists_eq_forall_mem_Icc_hasDerivWithinAt, IsPicardLindelof.picard_eq_of_hasDerivAt, ODE.picard, ContractingWith.tendsto_iterate_fixedPoint, ContractingWith.exists_fixedPoint, IsPicardLindelof.FunSpace.exists_contractingWith_iterate_next, IsPicardLindelof.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 |
| Q205692 | Poisson distribution | poissonMeasure, poissonMeasure_singleton, 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.constantCoeff, 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, Nat.ofDigits_digits, taylor_mean_remainder, polynomialFunctions_closure_eq_top, Matrix.charpoly, minpoly |
| 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, 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.isPrime_bot, PrimeSpectrum.instIsEmpty, 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, 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.setOf_prime_and_eq_mod_infinite, 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, Rat.AbsoluteValue.equiv_real_or_padic, Prime, Irreducible, Prime.irreducible, Nat.Prime.sq_add_sq, Ideal.IsPrime, Submodule.isLasker, PrimeSpectrum, Sylow.exists_subgroup_card_pow_prime, isCyclic_of_prime_card, Nat.FermatPsp, 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.measure_biUnion_finset_eq_sum_inter, 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 | MeasureTheory.uniformOn_univ, ProbabilityTheory.strong_law_ae |
| Q623472 | Probability space | MeasureTheory.IsProbabilityMeasure, MeasurableSpace, MeasurableSet, MeasureTheory.ProbabilityMeasure, MeasureTheory.MeasureSpace, MeasurableSet.iInter, PMF, MeasureTheory.Measure.IsComplete, Measurable, MeasureTheory.Measure.map, MeasurableSpace.measurableSet_top, MeasureTheory.borel, ProbabilityTheory.cond, ProbabilityTheory.cond_isProbabilityMeasure, ProbabilityTheory.IndepSet, ProbabilityTheory.IndepFun, Disjoint, MeasureTheory.measure_union, Set.inter |
| Q5862903 | Probability theory | MeasurableSet, IsProbabilityMeasure, 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 |
| Q901718 | Product (mathematics) | mul_comm, Nat.prod_primeFactorsList, Finset.prod, Finset.prod_empty, ZMod, MeasureTheory.convolution, Real.fourier_mul_convolution_eq, Polynomial.mul_def, Module, InnerProductSpace, norm_eq_sqrt_re_inner, InnerProductGeometry.angle, EuclideanSpace.inner_eq_star_dotProduct, crossProduct, triple_product_eq_det, LinearMap, LinearMap.comp, Matrix.mul, 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.instProjectivePlaneDualDual, 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 |
| 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 |
| Q978505 | Pullback (differential geometry) | ContMDiffVectorBundle.pullback, ContinuousMultilinearMap.compContinuousLinearMap, ContinuousAlternatingMap.compContinuousLinearMapCLM, mfderiv, extDeriv_pullback |
| Q837863 | Pure mathematics | irrational_sqrt_two |
| Q11518 | Pythagorean theorem | EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two, PythagoreanTriple, 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, RiemannianBundle |
| 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, ModularGroup, 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 |
| Q15909572 | Quadratic formula | quadratic_eq_zero_iff, discrim |
| Q50695 | Quadratic function | quadratic_eq_zero_iff, Polynomial.eq_quadratic_of_degree_le_two, QuadraticForm, Function.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, legendreSym.at_neg_one, ZMod.pow_card_sub_one_eq_one, legendreSym, ZMod.exists_sq_eq_neg_two_iff, jacobiSym.quadratic_reciprocity, jacobiSym |
| Q36810 | Quadrilateral | EuclideanGeometry.Cospherical.two_zsmul_oangle_eq, EuclideanGeometry.mul_dist_le_mul_dist_add_mul_dist |
| 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 |
| 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, Basis.extend |
| Q854531 | Real analysis | ConditionallyCompleteLinearOrderedField, isLUB_csSup, Real.metricSpace, Filter.Tendsto, Bornology.IsBounded, Monotone, CauchySeq, Real.instCompleteSpace, tendsto_atTop_ciSup, tendsto_pi_nhds, TendstoUniformly, Metric.isCompact_iff_isClosed_bounded, IsSeqCompact, isCompact_iff_finite_subcover, IsCompact.isComplete, IsCompact.image, ContinuousOn, Continuous, UniformContinuous, CompactSpace.uniformContinuous_of_continuous, AbsolutelyContinuousOnInterval, AbsolutelyContinuousOnInterval.uniformContinuousOn, HasDerivAt, DifferentiableAt.continuousAt, ContDiff, AnalyticOn, Summable, hasSum_geometric_of_lt_one, Real.not_summable_one_div_natCast, Summable.of_norm, taylorWithinEval, AnalyticAt, fourierCoeff, BoxIntegral.TaggedPrepartition, BoxIntegral.integralSum, BoxIntegral.integral, intervalIntegral.integral_eq_sub_of_hasDerivAt, MeasureTheory.Measure, Distribution |
| 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.choose_succ_succ, fwdDiff |
| Q752532 | Regular language | Language.IsRegular, NFA.reverse |
| Q389208 | Repeating decimal | Irrational |
| 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 |
| Q7322955 | Ricci calculus | TensorProduct.contractLeft, 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, riemannZeta_ne_zero_of_one_le_re |
| 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, LSeries_zeta_mul_Lseries_moebius, mellin, hurwitzZeta |
| Q161172 | Ring (mathematics) | Ring, CommRing, NonUnitalRing, DivisionRing, Int.instCommRing, ZMod, Matrix.instRing, Rat.instField, Algebra, Polynomial, ContinuousMap.instCommRing, Pi.ring, AddMonoid.End, MonoidAlgebra, Finset.prod, Monoid.npow, IsNilpotent, IsIdempotentElem, IsUnit, Subring, Subring.instCompleteLattice, Subring.closure, Subring.center, Ideal.span, IsSimpleRing, IsSimpleRing.isField, IsNoetherianRing, IsSemiprimaryRing.isNoetherian_iff_isArtinian, Ideal.IsPrime, RingHom, RingEquiv, Int.castRingHom, frobenius, AlgEquiv, Representation, RingHom.ker, Ideal.Quotient, Ideal.Quotient.lift, RingHom.quotientKerEquivOfSurjective, Module, Module.compHom, Prod.instRing, Ideal.quotientInfRingEquivPiQuotient, Polynomial.instIsDomain, Polynomial.aeval, MvPolynomial.aeval_unique, MvPolynomial.vanishingIdeal_zeroLocus_eq_radical, PowerSeries, Module.End, Matrix.toLinAlgEquiv, IsSimpleModule.instDivisionRingEnd, 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, IsDomain, IsPrincipalIdealRing, UniqueFactorizationMonoid, Module.equiv_free_prod_directSum, LittleWedderburn, Module.Free.of_divisionRing, IsSemisimpleModule, DivisionRing.toIsSemisimpleRing, Matrix.instIsSemisimpleRing, 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.Base.flip, LieAlgebra.IsKilling.isSimple_iff_isIrreducible, RootPairing.InvariantForm.exists_apply_eq_or |
| Q165498 | Schrödinger equation | Module.End.HasEigenvector, MeasureTheory.pdf |
| Q6500908 | Self-adjoint operator | IsSelfAdjoint, LinearMap.IsSymmetric.eigenvectorBasis_apply_self_apply, LinearPMap.graph, LinearPMap.adjoint, LinearMap.IsSymmetric, LinearPMap.IsSelfAdjoint, LinearMap.IsSymmetric.continuous, ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric, realPart_add_I_smul_imaginaryPart, ContinuousLinearMap.IsPositive.isSelfAdjoint, LinearMap.IsSymmetric.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 |
| Q1140985 | Separation axiom | SeparatedNhds, T0Space, R0Space, T1Space, t1Space_iff_t0Space_and_r0Space, R1Space, R1Space.toR0Space, T2Space, R1Space.t2Space_iff_t0Space, T2Space.t1Space, T25Space, T25Space.t2Space, RegularSpace, RegularSpace.toR1Space, 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, 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, tendsto_of_subseq_tendsto, CauchySeq, cauchySeq_tendsto_of_complete, CompleteSpace, tsum, Finset.sum, HasSum, isCompact_iff_isSeqCompact, continuous_iff_seqContinuous, 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, Nat.instInfinite, 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, Function, 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, Basis.ofVectorSpace, Ideal.exists_le_maximal, WellOrderingRel, Nat.lt_wfRel, Ordinal.induction |
| Q12482 | Set theory | Cardinal, Cardinal.not_countable_real, Cardinal.cantor, Ordinal, Set.Mem, Set.Subset, Set.ssubset_iff_subset_ne, Set.union, Set.inter, Set.diff, Set.compl, symmDiff, Set.prod, Set.instEmptyCollectionSet, Set.powerset, ZFSet.rank |
| Q33100 | Seven Bridges of Königsberg | SimpleGraph.Walk.IsTrail.even_countP_edges_iff, SimpleGraph.Walk.IsEulerian.even_degree_iff, SimpleGraph.degree, SimpleGraph.Walk.IsEulerian |
| 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.sheafificationAdjunction, CategoryTheory.sheafHom, TopCat.Presheaf.pushforward, TopCat.Sheaf.pullback, CategoryTheory.Presheaf.isSheaf_iff_isLimit, AlgebraicGeometry.RingedSpace, AlgebraicGeometry.LocallyRingedSpace, SheafOfModules, CategoryTheory.GrothendieckTopology |
| Q940334 | Shor's algorithm | orderOf, sq_sub_sq, Real.exists_rat_eq_convergent |
| 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, Basis.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 |
| Q190667 | Slide rule | Real.log_mul, quadratic_eq_zero_iff, Real.logb, div_add_one |
| Q759832 | Solvable group | IsSolvable, derivedSeries, CommGroup.isSolvable, IsNilpotent.to_isSolvable, solvable_of_ker_le_range, Equiv.Perm.fin_5_not_solvable, Equiv.Perm.not_solvable, IsZGroup, subgroup_solvable_of_solvable, solvable_of_surjective, solvable_prod |
| 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, 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, EuclideanSpace.volume_ball, EuclideanSpace.instChartedSpaceSphere, isCompact_sphere |
| Q203218 | Spherical coordinate system | Metric.sphere |
| Q877100 | Spherical harmonics | InnerProductSpace.HarmonicAt, MvPolynomial.IsHomogeneous |
| Q164 | Square | irrational_sqrt_two, IsSquare, DihedralGroup, 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 |
| Q159375 | Standard deviation | ProbabilityTheory.variance_eq_sub, ProbabilityTheory.meas_ge_le_variance_div_sq |
| 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 |
| 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.isProjectiveLimit_infinitePi |
| Q939927 | Stone–Weierstrass theorem | polynomialFunctions_closure_eq_top, ContinuousMap.instSeparableSpace, ContinuousMap.instNormedAlgebra, Subalgebra.SeparatesPoints, subalgebra_topologicalClosure_eq_top_of_separatesPoints, ZeroAtInftyContinuousMap, StarSubalgebra.adjoin, fourierSubalgebra_closure_eq_top, ContinuousMap.starSubalgebra_topologicalClosure_eq_top_of_separatesPoints, ContinuousMap.instLattice, ContinuousMap.sublattice_closure_eq_top |
| Q33198 | String theory | Matrix, Group, DihedralGroup, IsSimpleGroup |
| 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 |
| 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.instHasSSubset, Set.powerset, Set.instBooleanAlgebra, Set.inter_eq_left, Set.union_eq_right |
| Q40754 | Subtraction | SubNegMonoid, sub_eq_add_neg, neg_sub, sub_zero, Order.pred |
| Q484298 | Surface (topology) | chartAt, ModelWithCorners.IsBoundaryPoint, ModelWithCorners.IsInteriorPoint, SmoothBumpCovering.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.Types.epi_iff_surjective, CategoryTheory.IsSplitEpi.epi, CategoryTheory.SplitEpi.section_, CategoryTheory.IsSplitEpi, Cardinal.mk_le_of_surjective, Fintype.injective_iff_surjective_of_equiv, Function.Surjective.comp, Set.rangeFactorization_surjective, Setoid.quotientKerEquivOfSurjective |
| Q1057919 | Sylow theorems | IsPGroup, Sylow, Sylow.card_eq_multiplicity, Sylow.nonempty, exists_prime_orderOf_dvd_card, Sylow.isPretransitive_of_finite, card_sylow_modEq_one, exists_subgroup_card_pow_prime, Sylow.normal_of_subsingleton, Sylow.card_dvd_index, IsPGroup.exists_le_sylow, Nat.prime_iff_fac_equiv_neg_one, ker_transferSylow_isComplement', IsPGroup.card_modEq_card_fixedPoints, 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, Equiv.Perm.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, Equiv.Perm.alternatingGroup.isSimpleGroup, Subgroup, Equiv.Perm.isCoatom_stabilizer, Sylow.isPGroup', IteratedWreathProduct, MulAction.IsPretransitive, Polynomial.Gal.galAction_isPretransitive, Subgroup.zpowers, Equiv.Perm.lcm_cycleType, MonoidAlgebra.instIsSemisimpleModule (Maschke) |
| 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 |
| Q746550 | Tangent bundle | TangentBundle, Bundle.TotalSpace.mk, Bundle.TotalSpace.proj, ContMDiff.contMDiff_tangentMap, tangentBundleCore, TangentSpace.vectorBundle, ContMDiffSection |
| 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, 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, Matrix.dotProductBilin, LinearMap.BilinForm, TensorAlgebra, TensorProduct.addCommMonoid, TensorProduct.tmul, contractLeft, PiTensorProduct |
| Q1163016 | Tensor product | TensorProduct, TensorProduct.tmul, TensorProduct.lift.equiv, Basis.tensorProduct, 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, SymmetricAlgebra |
| Q214856 | Tessellation | DiscreteTiling.Prototile |
| Q160003 | Tetrahedron | Affine.Simplex, Affine.Simplex.circumsphere, Affine.Simplex.Regular, Affine.Simplex.mongePoint, Affine.Simplex.dist_point_centroid_eq_mul_dist_centroid_faceOppositeCentroid, 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 | Turing.TM2ComputableInPolyTime |
| 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_1, 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, Real.instIsTopologicalAddGroup, Matrix.GeneralLinearGroup, Matrix.orthogonalGroup, LieGroup, PadicInt, ProfiniteGrp, Homeomorph.mulLeft, Homeomorph.inv, IsTopologicalGroup.rightUniformSpace, Subgroup.instIsTopologicalGroup, 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.instCompleteLatticeTopologicalSpace, Continuous, Continuous.isOpen_preimage, Homeomorph, TopCat, FinTopCat, CofiniteTopology, Ordinal.instTopologicalSpace, sierpinskiSpace, instTopologicalSpaceSubtype, instTopologicalSpaceProd, instTopologicalSpaceQuotient, PseudoMetricSpace.toUniformSpace, Real.instTopologicalSpace, TopologicalSpace.IsTopologicalBasis, IsTopologicalGroup, PrimeSpectrum.zariskiTopology, SpectralSpace, specializationPreorder, Filter.instTopologicalSpaceFilter |
| Q42989 | Topology | TopologicalSpace, Homeomorph, ContinuousMap.HomotopyEquiv, IsOpen, IsClosed, IsClopen, TopologicalSpace.OpenNhds, Continuous, ChartedSpace, IsCompact, IsConnected, MetricSpace, Metric.isOpen_iff, subgroupIsFreeOfIsFree, CategoryTheory.GrothendieckTopology |
| Q369377 | Total order | LinearOrder, extend_partialOrder, IsStrictTotalOrder, le_iff_lt_or_eq, asymm_of_isTrans_of_irrefl, Subtype.instLinearOrder, Empty.instLinearOrder, 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, Fintype.to_wellFoundedLT, monoEquivOfFin, StrictMono.orderIsoOfSurjective, Set.Ioo, OrderTopology, OrderTopology.t5Space, ConditionallyCompleteLinearOrder, compactSpace_of_completeLinearOrder, Sum.Lex.linearOrder, Sigma.Lex, Prod.Lex.instLinearOrder, Prod.instPartialOrder, instIsStrictWeakOrder, PartialOrder, IsOrderedMonoid |
| Q173091 | Transcendental number | Transcendental, Transcendental.irrational, transcendental_liouvilleNumber, Liouville, Liouville.transcendental, Algebraic.countable |
| Q840810 | Transfinite induction | Ordinal.induction, Ordinal.limitRecOn, Basis.ofVectorSpace, WellFoundedLT.fix, IsWellFounded.fix |
| Q46303 | Trapezoid | trapezoidal_integral |
| 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, abs_norm_sub_norm_le, lipschitzWith_one_norm |
| Q93344 | Trigonometric functions | Real.sin, Real.sin_pi_div_two_sub, Real.sin_sq_add_cos_sq, Real.sin_periodic, Real.cos_pi_div_four, Real.sin_eq_tsum, Complex.meromorphic_tan, Complex.pi_mul_cot_pi_q_exp, Complex.tendsto_euler_sin_prod, Complex.exp_mul_I, Complex.sin, Complex.sin_eq, Real.sin_eq_zero_iff, Real.cos_neg, Complex.sin_add, Complex.cos_two_mul, Real.sin_eq_two_mul_tan_half_div_one_add_tan_half_sq, 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 |
| 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 |
| 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 |
| 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, VectorBundle.prod, Bundle.ContinuousLinearMap.vectorBundle, VectorBundle.pullback, 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 |
| Q125977 | Vector space | Module, AddCommMonoid, SMul.smul, Finsupp.linearCombination, LinearIndependent, Submodule, Submodule.span, Module.Basis, exists_basis, mk_eq_mk_of_basis, Basis.repr, Prod.module, Pi.module, Algebra, LinearMap.ker, LinearMap, LinearEquiv, Module.Dual, nonempty_linearEquiv_of_finrank_eq, LinearMap.toMatrix, LinearMap.isUnit_iff_isUnit_det, Module.End.HasEigenvector, LinearMap.charpoly, Module.End.eigenspace, Submodule.Quotient, 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, type_nat_lt, PrincipalSeg.ofElement, InitialSeg.isLowerSet_range, ZFSet.IsOrdinal, PrincipalSeg.irrefl, InitialSeg.total, InitialSeg.image_Iio, Ordinal, Preorder.topology, IsCofinal, Ordinal.type_fintype |
| 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 |
| Q899731 | Zeros and poles | MeromorphicOn, MeromorphicAt.inv_iff, AnalyticOnNhd, meromorphicOrderAt, MeromorphicAt.eventually_eq_zero_or_eventually_ne_zero |
| Q290810 | Zorn's lemma | zorn_le, 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, Ideal.exists_maximal, isCompact_univ_pi, ChainCompletePartialOrder.nonempty_fixedPoints_of_inflationary, exists_extension_of_le_sublinear, Ultrafilter.exists_le |
| Q8078429 | Étale cohomology | AlgebraicGeometry.Scheme.Etale, AlgebraicGeometry.Scheme.EllAdicCohomology, AlgebraicGeometry.Scheme.ellAdicSheaf |