| 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 |
| 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 |
| Q202 | 4 | Nat.sum_four_squares, IsKleinFour |
| 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 |
| 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 |
| 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 |
| 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 |
| Q333464 | Analysis of algorithms | Asymptotics.IsBigO |
| 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 |
| 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 |
| Q755991 | Atiyah–Singer index theorem | IsManifold, ContMDiffVectorBundle |
| Q17736 | Axiom | FirstOrder.Language.Theory, ConditionallyCompleteLinearOrderedField.uniqueOrderRingIso, FirstOrder.Language.Theory.exists_elementaryEmbedding_card_eq |
| 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 |
| 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 |
| 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 |
| Q185547 | Binomial distribution | ProbabilityTheory.binomial, PMF.bernoulli, PMF.binomial_one_eq_bernoulli, PMF.binomial_apply, ProbabilityTheory.tendsto_choose_mul_pow_of_tendsto_mul_atTop |
| 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 |
| 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 |
| 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 |
| 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 |
| Q166314 | Chaos theory | MulAction.IsTopologicallyTransitive |
| 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 |
| Q5150824 | Combinatorial design | Configuration.ProjectivePlane, Configuration.HasLines.card_le |
| 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 |
| 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 |
| Q319141 | Conjecture | FermatLastTheorem, SimplyConnectedSpace.nonempty_homeomorph_sphere_three, ContinuousMap.HomotopyEquiv.nonempty_homeomorph_sphere, RiemannHypothesis |
| 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 |
| 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 |
| 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 |
| Q7874246 | Coxeter group | CoxeterMatrix.Group, CoxeterSystem, CoxeterSystem.simple_mul_simple_self, CoxeterMatrix, CoxeterSystem.length, CoxeterSystem.IsReduced, CoxeterSystem.lengthParity |
| 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 |
| 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 |
| 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 |
| Q188444 | Differential geometry | IsRiemannianManifold, LieGroup, GroupLieAlgebra |
| Q2502381 | Differential geometry of surfaces | ContDiffOn, EuclideanSpace.instIsManifoldSphere, VectorField.mlieBracket, RiemannianMetric, pathELength_comp_of_monotoneOn, EuclideanGeometry.law_cos |
| 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 |
| Q121416 | Discrete mathematics | peirce |
| 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 |
| 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 |
| 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₂ |
| Q1332450 | Elliptic geometry | Projectivization.equivSubmodule |
| 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 |
| 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 |
| 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 |
| 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 |
| 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 |
| 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 |
| 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 |
| Q81392 | Fractal | MeasureTheory.dimH, NowhereDifferentiable.exists_uniformContinuous_and_not_differentiableAt, cantorSet |
| 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 |
| Q44455 | Game theory | Sion.exists_isSaddlePointOn |
| 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 |
| Q213488 | Geodesic | Manifold.pathELength, Manifold.riemannianEDist |
| Q2662474 | Geometric group theory | SimpleGraph.mulCayley, Int.instAddCommGroup, FreeGroup, Monoid.CoprodI, Equiv.Perm, CoxeterSystem |
| Q8087 | Geometry | ChartedSpace, IsManifold, InnerProductGeometry.angle, EuclideanGeometry.angle, EuclideanSpace.dist_eq, MetricSpace, MeasureTheory.Measure, Similar, MvPolynomial.vanishingIdeal_zeroLocus_eq_radical, Convex |
| 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 |
| 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 |
| 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 |
| Q200787 | Gödel's incompleteness theorems | FirstOrder.Language.Theory.IsComplete, FirstOrder.Field.ACF_isComplete, Nat.Partrec.Code.halting_problem |
| 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 |
| 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 |
| 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 |
| 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 |
| 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 |
| Q187631 | Interpolation | AffineMap.lineMap, AffineMap.lineMap_apply_ring, Lagrange.interpolate, Lagrange.eq_interpolate_iff |
| Q16743426 | Introduction to gauge theory | Circle.instCommGroup, CommGroup, Group, Int.instAddCommGroup |
| 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' |
| 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 |
| Q199691 | Laplace transform | ProbabilityTheory.mgf |
| Q484637 | Linear equation | AffineMap |
| Q202843 | Linear programming | IsMinOn.of_isLocalMin_of_convex_univ |
| Q8078 | Logic | em, inf_sup_left |
| 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 |
| 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 |
| Q395 | Mathematics | FermatLastTheorem, Module, BooleanAlgebra, Function.cantor_surjective, Module.Flat.of_free, Nat.exists_infinite_primes |
| 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 |
| Q226995 | Median | ConvexOn.map_integral_le |
| Q464794 | Minkowski space | LinearMap.BilinForm.IsOrtho, LinearMap.BilinForm.toDual, LinearMap.BilinForm.nondegenerate_iff_ker_eq_bot |
| 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 |
| 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 |
| Q232207 | Monte Carlo method | ProbabilityTheory.strong_law_ae |
| Q190529 | Nicolas Bourbaki | one_add_one_eq_two, Set.empty_def, Function.Bijective, Metric.ball |
| 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 |
| 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 |
| 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 |
| 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 |
| Q746242 | P versus NP problem | ComputablePred.halting_problem |
| Q48297 | Parabola | AffineMap |
| Q1413083 | Parameter | Real.logb, Nat.descFactorial, circleMap, ProbabilityTheory.poissonPMF, ProbabilityTheory.gaussianReal |
| Q1187620 | Perfect graph | SimpleGraph.IsClique, SimpleGraph.cliqueNum, SimpleGraph.Coloring, SimpleGraph.chromaticNumber, SimpleGraph.cliqueNum_le_chromaticNumber, PartialOrder, IncompRel, IsChain, IsAntichain |
| 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 |
| 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 |
| 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 |
| 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 |
| 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 |
| Q837863 | Pure mathematics | irrational_sqrt_two |
| Q15909572 | Quadratic formula | quadratic_eq_zero_iff, discrim |
| 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 |
| Q918099 | Ramsey's theorem | Finite.exists_infinite_fiber |
| Q23937546 | Real projective line | Projectivization, Projectivization.equivSubmodule, projectivizationSetoid, Matrix.op_smul_eq_vecMul, Projectivization.generalLinearGroup_smul_def, Matrix.ProjGenLinGroup, OnePoint.smul_some_eq_ite |
| 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 |
| 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 |
| 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 |
| 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 |
| 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 |
| 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 |
| Q133327 | Spacetime | EuclideanSpace.dist_eq, Isometry.dist_eq, IsRiemannianManifold |
| 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 |
| Q203218 | Spherical coordinate system | Metric.sphere |
| Q164 | Square | irrational_sqrt_two, IsSquare, DihedralGroup, norm_add_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two |
| 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 |
| 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 |
| Q80918 | Stirling number | Nat.stirlingFirst, Nat.stirlingSecond, descPochhammer_zero, Ring.descPochhammer_eq_factorial_smul_choose |
| 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 |
| 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) |
| 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 |
| 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 |
| 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 |
| Q214856 | Tessellation | DiscreteTiling.Prototile |
| 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 |
| Q42989 | Topology | TopologicalSpace, Homeomorph, ContinuousMap.HomotopyEquiv, IsOpen, IsClosed, IsClopen, TopologicalSpace.OpenNhds, Continuous, ChartedSpace, IsCompact, IsConnected, MetricSpace, Metric.isOpen_iff, subgroupIsFreeOfIsFree, CategoryTheory.GrothendieckTopology |
| Q173091 | Transcendental number | Transcendental, Transcendental.irrational, transcendental_liouvilleNumber, Liouville, Liouville.transcendental, Algebraic.countable |
| 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 |
| 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 |
| Q163310 | Turing machine | Turing.TM0.Machine, ComputablePred.halting_problem, Turing.TM0.Cfg |
| 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 |
| 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 |
| 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 |