Q204
formalized as: zero_add
formalized as: mul_zero
formalized as: Nat.zero_le
formalized as: Even.zero
formalized as: Ideal.bot_prime
formalized as: add_zero
formalized as: sub_zero
formalized as: inv_zero
formalized as: pow_zero
formalized as: Finset.prod_empty
formalized as: Nat.factorial_zero
formalized as: Cardinal.mk_eq_zero
formalized as: Ordinal.bot_eq_zero
formalized as: Zero
formalized as: Pi.zero_apply
formalized as: CategoryTheory.Limits.IsZero
formalized as: zero_div
formalized as: neg_zero

Q199
formalized as: Nat.succ
formalized as: one_mul
formalized as: one_pow
formalized as: MulOneClass
formalized as: IsUnit
formalized as: Nat.factorial_one
formalized as: Finset.prod_empty
formalized as: unitInterval
formalized as: IsProbabilityMeasure

Q200
formalized as: Nat.succ
formalized as: Nat.Prime.even_iff
formalized as: even_iff_two_dvd
formalized as: ZMod.instField
formalized as: ZMod.intCast_zmod_eq_zero_iff_dvd
formalized as: CharTwo.add_self_eq_zero
formalized as: Function.Involutive

Q202
formalized as: Nat.sum_four_squares
formalized as: IsKleinFour

Q181296
formalized as: CommGroup
formalized as: PUnit.commGroup
formalized as: Int.instAddCommGroup
formalized as: IsCyclic.commGroup
formalized as: NonUnitalNonAssocRing
formalized as: instCommGroupUnits
formalized as: Subgroup.normal_of_isMulCommutative
formalized as: Subgroup.toCommGroup
formalized as: CommGroup.is_simple_iff_prime_card
formalized as: forget₂AddCommGroupIsEquivalence
formalized as: AddCommGroup.toIntModule
formalized as: AddCommGroup.equiv_free_prod_directSum_zmod
formalized as: AddMonoidHom.add
formalized as: Module.rank
formalized as: Module.rank_eq_zero_iff_isTorsion
formalized as: Subgroup.center
formalized as: Subgroup.center_eq_top_iff
formalized as: commGroupOfCyclicCenterQuotient
formalized as: AddCommGroup.equiv_directSum_zmod_of_finite
formalized as: isCyclic_of_prime_card
formalized as: IsPGroup.commutative_of_card_eq_prime_sq
formalized as: ZMod.chineseRemainder
formalized as: AddGroup.FG
formalized as: FreeAbelianGroup.lift
formalized as: Module.Basis.SmithNormalForm
formalized as: Int.instIsAddCyclic
formalized as: DivisibleBy
formalized as: Monoid.IsTorsion
formalized as: Monoid.IsTorsionFree
formalized as: Submodule.instIsTorsionFree
formalized as: AddCommGrpCat.instAbelian

Q2553675
formalized as: Matrix.transvection

Q180969
formalized as: MvPolynomial
formalized as: MvPolynomial.zeroLocus
formalized as: MvPolynomial.vanishingIdeal
formalized as: PrimeSpectrum.zariskiTopology
formalized as: MvPolynomial.vanishingIdeal_zeroLocus_eq_radical
formalized as: MvPolynomial.isNoetherianRing
formalized as: IsIrreducible
formalized as: TopologicalSpace.NoetherianSpace.exists_finset_irreducible
formalized as: PrimeSpectrum.isIrreducible_iff_vanishingIdeal_isPrime
formalized as: ContinuousMap.exists_restrict_eq
formalized as: AlgebraicGeometry.Scheme.functionField
formalized as: AlgebraicGeometry.Scheme.RationalMap
formalized as: Projectivization
formalized as: ProjectiveSpectrum.zeroLocus
formalized as: AlgebraicGeometry.Scheme
formalized as: AlgebraicGeometry.AffineScheme.equivCommRingCat

Q168817
formalized as: IsAlgebraic
formalized as: isAlgebraic_int
formalized as: algebraicClosure
formalized as: Transcendental
formalized as: isAlgebraic_rat
formalized as: GaussianInt
formalized as: Real.isAlgebraic_cos_rat_mul_pi
formalized as: IsFractionRing.isAlgebraic_iff
formalized as: minpoly
formalized as: Algebraic.countable
formalized as: IntermediateField.adjoin.finiteDimensional
formalized as: IntermediateField.finiteDimensional_adjoin
formalized as: Subalgebra.algebraicClosure
formalized as: algebraicClosure.isAlgClosure
formalized as: IsIntegral
formalized as: integralClosure
formalized as: NumberField.RingOfIntegers

Q613048
formalized as: PythagoreanTriple
formalized as: NumberField.Units.exist_unique_eq_mul_prod
formalized as: Real.exists_int_int_abs_mul_sub_le
formalized as: Ideal
formalized as: Prime
formalized as: Associated
formalized as: UniqueFactorizationMonoid
formalized as: Irreducible
formalized as: Ideal.uniqueFactorizationMonoid
formalized as: Nat.Prime.sq_add_sq
formalized as: FractionalIdeal
formalized as: ClassGroup
formalized as: NumberField.classNumber
formalized as: NumberField.InfinitePlace.IsReal
formalized as: NumberField.InfinitePlace.card_add_two_mul_card_eq_rank
formalized as: NumberField.mixedEmbedding
formalized as: NumberField.mixedEmbedding.mixedSpace
formalized as: NumberField.discr
formalized as: padicNorm
formalized as: Rat.AbsoluteValue.equiv_real_or_padic
formalized as: NumberField.FinitePlace
formalized as: NumberField.AdeleRing
formalized as: Int.isUnit_iff
formalized as: NumberField.Units.regulator
formalized as: NumberField.dedekindZeta
formalized as: IsDedekindDomain.HeightOneSpectrum.adicCompletion
formalized as: NumberField.RingOfIntegers.instFintypeClassGroup
formalized as: legendreSym.quadratic_reciprocity
formalized as: NumberField.tendsto_sub_one_mul_dedekindZeta_nhdsGT

Q212803
formalized as: subgroupIsFreeOfIsFree
formalized as: HomotopyGroup
formalized as: FundamentalGroup
formalized as: singularHomologyFunctor
formalized as: HomologicalComplex.homology
formalized as: IsManifold
formalized as: Geometry.SimplicialComplex
formalized as: CWComplex
formalized as: AddCommGroup.equiv_free_prod_directSum_zmod
formalized as: Complex.isAlgClosed

Q648995
formalized as: MvPolynomial.vanishingIdeal_zeroLocus_eq_radical
formalized as: MvPolynomial.zeroLocus
formalized as: MvPolynomial.vanishingIdeal
formalized as: ProjectiveSpectrum.zeroLocus
formalized as: WeierstrassCurve.IsElliptic
formalized as: AlgebraicGeometry.Scheme

Q8366
formalized as: List.mergeSort

Q333464
formalized as: Asymptotics.IsBigO

Q58413
formalized as: EuclideanGeometry.Sphere.thales_theorem
formalized as: EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two
formalized as: EuclideanGeometry.Sphere.IsTangentAt.mem_and_mem_iff_eq
formalized as: irrational_sqrt_natCast_iff
formalized as: Nat.gcd
formalized as: Nat.exists_infinite_primes
formalized as: Even.mul_right
formalized as: Int.ModEq
formalized as: DedekindCut

Q11352
formalized as: EuclideanGeometry.angle
formalized as: Orientation.oangle
formalized as: EuclideanGeometry.angle_add_of_ne_of_ne
formalized as: Sbtw.oangle_eq_left_right
formalized as: EuclideanGeometry.angle_add_angle_add_angle_eq_pi
formalized as: Real.Angle.angle_eq_iff_two_pi_dvd_sub
formalized as: InnerProductGeometry.cos_angle
formalized as: InnerProductGeometry.angle

Q11205
formalized as: Nat
formalized as: Int
formalized as: Cardinal
formalized as: Ordinal
formalized as: Rat
formalized as: Irrational
formalized as: Real
formalized as: MulOneClass
formalized as: mul_inv_cancel
formalized as: CommMagma
formalized as: Semigroup
formalized as: Add
formalized as: Finset.sum
formalized as: sub_eq_add_neg
formalized as: add_zero
formalized as: add_comm
formalized as: Mul
formalized as: div_eq_mul_inv
formalized as: mul_one
formalized as: mul_comm
formalized as: Monoid.npow
formalized as: Real.rpow
formalized as: Real.log
formalized as: nsmul_eq_mul
formalized as: npowBinRec
formalized as: Nat.primeFactorsList_unique
formalized as: Nat.exists_infinite_primes
formalized as: FermatLastTheorem
formalized as: div_add_div_same
formalized as: div_mul_div_comm
formalized as: Real.rpow_pos_of_pos
formalized as: round
formalized as: ZMod
formalized as: Matrix
formalized as: Nat.zero
formalized as: Nat.succ
formalized as: Nat.succ_injective
formalized as: Nat.succ_ne_zero
formalized as: Nat.rec

Q755991
formalized as: IsManifold
formalized as: ContMDiffVectorBundle

Q17736
formalized as: FirstOrder.Language.Theory
formalized as: ConditionallyCompleteLinearOrderedField.uniqueOrderRingIso
formalized as: FirstOrder.Language.Theory.exists_elementaryEmbedding_card_eq

Q220680
formalized as: ContractingWith
formalized as: ContractingWith.exists_fixedPoint
formalized as: ContractingWith.apriori_dist_iterate_fixedPoint_le
formalized as: LipschitzWith
formalized as: IsPicardLindelof.exists_eq_forall_mem_Icc_hasDerivWithinAt
formalized as: HasStrictFDerivAt.toOpenPartialHomeomorph
formalized as: ContractingWith.isFixedPt_fixedPoint_iterate

Q182505
formalized as: ProbabilityTheory.cond_eq_inv_mul_cond_mul
formalized as: ProbabilityTheory.cond
formalized as: ProbabilityTheory.cond_mul_eq_inter
formalized as: ProbabilityTheory.posterior_eq_withDensity
formalized as: MeasureTheory.Measure.withDensity_rnDeriv_eq

Q214728
formalized as: AffineMap.lineMap
formalized as: AffineMap.lineMap_apply_module
formalized as: bernsteinPolynomial

Q4907197
formalized as: Function.Injective
formalized as: Function.Surjective
formalized as: Function.Bijective
formalized as: Function.injective_iff_hasLeftInverse
formalized as: Equiv.ofInjective
formalized as: Function.Injective.comp
formalized as: Function.Embedding.injective
formalized as: Function.surjective_iff_hasRightInverse
formalized as: Setoid.quotientKerEquivOfSurjective
formalized as: Function.Surjective.comp
formalized as: Function.bijective_iff_has_inverse
formalized as: Function.Bijective.comp
formalized as: Equiv.Perm.permGroup
formalized as: Cardinal.eq
formalized as: Cardinal.le_def
formalized as: Function.bijective_id
formalized as: Real.expOrderIso
formalized as: Set.image_preimage_subset
formalized as: CategoryTheory.Types.mono_iff_injective

Q185547
formalized as: ProbabilityTheory.binomial
formalized as: PMF.bernoulli
formalized as: PMF.binomial_one_eq_bernoulli
formalized as: PMF.binomial_apply
formalized as: ProbabilityTheory.tendsto_choose_mul_pow_of_tendsto_mul_atTop

Q4973304
formalized as: DistribLattice.booleanAlgebraOfComplemented
formalized as: BooleanAlgebra.toBooleanRing
formalized as: BooleanAlgebra
formalized as: PUnit.instBooleanAlgebra
formalized as: inf_eq_left
formalized as: BooleanAlgebra.toBoundedOrder
formalized as: compl_unique
formalized as: OrderDual.instBooleanAlgebra
formalized as: Bool.instBooleanAlgebra
formalized as: Set.instBooleanAlgebra
formalized as: TopologicalSpace.Clopens.instBooleanAlgebra
formalized as: instBooleanAlgebraSubtypeIsIdempotentElem
formalized as: BoundedLatticeHom
formalized as: map_compl'
formalized as: OrderIso
formalized as: BooleanRing.toBooleanAlgebra
formalized as: boolRingCatEquivBoolAlg
formalized as: Order.Ideal
formalized as: Order.Ideal.IsPrime
formalized as: Order.Ideal.IsMaximal
formalized as: Order.Ideal.IsPrime.isMaximal
formalized as: Order.PFilter
formalized as: Ultrafilter.exists_le
formalized as: GeneralizedBooleanAlgebra

Q1144897
formalized as: exists_mem_Icc_isFixedPt_of_mapsTo

Q263809
formalized as: CStarAlgebra
formalized as: ZeroAtInftyContinuousMap.instNonUnitalCommCStarAlgebra
formalized as: CStarRing.norm_star_mul_self
formalized as: StarAlgHom
formalized as: NonUnitalStarAlgHom.norm_apply_le
formalized as: StarAlgEquiv
formalized as: StarSubalgebra.cstarAlgebra
formalized as: IsSelfAdjoint
formalized as: nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts
formalized as: CStarAlgebra.increasingApproximateUnit
formalized as: Matrix.instCStarRing
formalized as: ContinuousLinearMap.instCStarAlgebra
formalized as: gelfandStarTransform
formalized as: VonNeumannAlgebra

Q729471
formalized as: Uncountable
formalized as: Function.cantor_surjective
formalized as: Cardinal.not_countable_real
formalized as: Cardinal.cantorFunction_injective
formalized as: Cardinal.cantor
formalized as: Cardinal.le_def
formalized as: Function.Embedding.schroeder_bernstein
formalized as: ComputablePred.halting_problem

Q4049983
formalized as: Cardinal.mk
formalized as: Cardinal.eq
formalized as: Set
formalized as: Cardinal.aleph0
formalized as: Function.Injective
formalized as: Function.Surjective
formalized as: Function.Bijective
formalized as: Cardinal.le_def
formalized as: schroeder_bernstein
formalized as: Ordinal.type
formalized as: WellOrderingRel
formalized as: Countable
formalized as: Set.Countable
formalized as: Rat
formalized as: Cardinal.mkRat
formalized as: IsAlgebraic
formalized as: Transcendental
formalized as: Algebraic.countable
formalized as: Uncountable
formalized as: Cardinal.not_countable_real
formalized as: Cardinal.mk_set_nat
formalized as: Cardinal.mk_real
formalized as: Cardinal.cantor
formalized as: Cardinal
formalized as: Nat.card
formalized as: Finite.injective_iff_surjective
formalized as: Cardinal.add_def
formalized as: Cardinal.mk_prod
formalized as: Finset.inclusion_exclusion_card_biUnion
formalized as: Finite
formalized as: Cardinal.aleph
formalized as: Ordinal
formalized as: Ordinal.omega0
formalized as: Ordinal.omega
formalized as: Cardinal.aleph_succ
formalized as: Cardinal.mem_range_aleph_iff
formalized as: Cardinal.mul_def
formalized as: Cardinal.sum_lt_prod
formalized as: Cardinal.add_eq_self
formalized as: Cardinal.mk_arrow
formalized as: Cardinal.power_zero
formalized as: Cardinal.mk_set
formalized as: not_small_cardinal
formalized as: Real
formalized as: Cardinal.continuum
formalized as: Cardinal.mk_Ioo_real
formalized as: Real.tanOrderIso
formalized as: cantorSet
formalized as: Cardinal.continuum_power_aleph0
formalized as: Cardinal.aleph0_lt_continuum
formalized as: Cardinal.beth
formalized as: ZFSet.omega
formalized as: ZFSet.powerset
formalized as: ZFSet.choice
formalized as: Cardinal.IsInaccessible
formalized as: ZFSet.vonNeumann
formalized as: Finset.card_lt_card

Q22952648
formalized as: Cardinal.continuum
formalized as: Cardinal.mk_set_nat
formalized as: Cardinal.eq
formalized as: Cardinal.mk_Ioo_real
formalized as: Cardinal.not_countable_real
formalized as: Cardinal.cantor
formalized as: Function.Embedding.schroeder_bernstein
formalized as: Cardinal.mk_real
formalized as: Cardinal.continuum_power_aleph0
formalized as: Cardinal.beth
formalized as: Cardinal.sum_lt_prod
formalized as: Algebraic.cardinalMk_of_countable_of_charZero

Q719395
formalized as: CategoryTheory.Category
formalized as: CategoryTheory.Functor
formalized as: Quiver.Hom
formalized as: CategoryTheory.SmallCategory
formalized as: CategoryTheory.LocallySmall
formalized as: CategoryTheory.types
formalized as: CategoryTheory.RelCat
formalized as: CategoryTheory.Discrete
formalized as: Preorder.smallCategory
formalized as: Quiver.IsThin
formalized as: CategoryTheory.SingleObj
formalized as: CategoryTheory.Iso
formalized as: CategoryTheory.Groupoid
formalized as: FundamentalGroupoid
formalized as: CategoryTheory.Paths
formalized as: Preord
formalized as: CategoryTheory.ConcreteCategory
formalized as: GrpCat
formalized as: Ab
formalized as: CategoryTheory.Cat
formalized as: CategoryTheory.Functor.category
formalized as: CategoryTheory.Category.opposite
formalized as: CategoryTheory.prod
formalized as: CategoryTheory.Quotient
formalized as: CategoryTheory.Over
formalized as: CategoryTheory.Under
formalized as: CategoryTheory.Localization
formalized as: CategoryTheory.Mono
formalized as: CategoryTheory.Epi
formalized as: CategoryTheory.IsSplitEpi
formalized as: CategoryTheory.IsSplitMono
formalized as: CategoryTheory.IsIso
formalized as: CategoryTheory.End
formalized as: CategoryTheory.End.monoid
formalized as: CategoryTheory.Aut
formalized as: CategoryTheory.IsSplitEpi.epi
formalized as: CategoryTheory.Preadditive
formalized as: CategoryTheory.Abelian
formalized as: AddCommGrpCat
formalized as: CategoryTheory.EnrichedCategory
formalized as: CategoryTheory.Limits.HasLimits
formalized as: CategoryTheory.Limits.Types.hasLimitsOfSize
formalized as: CategoryTheory.CartesianClosed

Q656772
formalized as: Matrix.aeval_self_charpoly
formalized as: Matrix.charpoly
formalized as: Matrix.pow_eq_aeval_mod_charpoly
formalized as: Matrix.minpoly_dvd_charpoly
formalized as: Matrix.charpoly_fin_two
formalized as: Matrix.adjugate
formalized as: Polynomial.div_modByMonic_unique
formalized as: Submodule.eq_bot_of_le_smul_of_le_jacobson_bot

Q166314
formalized as: MulAction.IsTopologicallyTransitive

Q193878
formalized as: Nat.chineseRemainderOfFinset
formalized as: ZMod.chineseRemainder
formalized as: Nat.chineseRemainder_modEq_unique
formalized as: Ideal.quotientInfToPiQuotient_surj
formalized as: Nat.chineseRemainder
formalized as: Nat.chineseRemainderOfList
formalized as: Ideal.quotientInfRingEquivPiQuotient
formalized as: Lagrange.interpolate
formalized as: Nat.chineseRemainder'
formalized as: Ideal.isCoprime_iff_exists
formalized as: Ideal.prod_eq_iInf_of_pairwise_isCoprime
formalized as: CompleteOrthogonalIdempotents
formalized as: linearIndependent_monoidHom

Q5150824
formalized as: Configuration.ProjectivePlane
formalized as: Configuration.HasLines.card_le

Q848569
formalized as: CompleteSpace
formalized as: CauchySeq
formalized as: IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed
formalized as: IsClosed.isComplete
formalized as: Real.instCompleteSpace
formalized as: Pi.complete
formalized as: BoundedContinuousFunction.instCompleteSpace
formalized as: Padic.instCompleteSpace
formalized as: IsCompact.isComplete
formalized as: isCompact_iff_totallyBounded_isComplete
formalized as: ProperSpace.isCompact_closedBall
formalized as: IsComplete.isClosed
formalized as: BaireSpace.of_completelyPseudoMetrizable
formalized as: ContractingWith.fixedPoint
formalized as: HasStrictFDerivAt.toOpenPartialHomeomorph
formalized as: UniformSpace.Completion
formalized as: Completion.extension_unique
formalized as: AbstractCompletion.compareEquiv
formalized as: Completion.instPseudoMetricSpace
formalized as: Completion.coe_isometry
formalized as: Real.equivCauchy
formalized as: Padic
formalized as: UniformSpace.Completion.instNormedSpace
formalized as: UniformSpace.Completion.innerProductSpace
formalized as: IsCompletelyMetrizableSpace
formalized as: PolishSpace
formalized as: IsTopologicalGroup.completeSpace_rightUniformSpace_iff_leftUniformSpace
formalized as: Cauchy

Q1148456
formalized as: Computable
formalized as: Nat.Partrec
formalized as: ComputablePred
formalized as: REPred
formalized as: Language
formalized as: Nat.Primrec.add
formalized as: Computable.comp
formalized as: ack
formalized as: ComputableIn

Q205084
formalized as: Turing.TM2ComputableInPolyTime
formalized as: Turing.TM0.Machine

Q319141
formalized as: FermatLastTheorem
formalized as: SimplyConnectedSpace.nonempty_homeomorph_sphere_three
formalized as: ContinuousMap.HomotopyEquiv.nonempty_homeomorph_sphere
formalized as: RiemannHypothesis

Q208416
formalized as: Cardinal.sum_lt_prod
formalized as: Cardinal.eq
formalized as: Cardinal.mkRat
formalized as: Cardinal.aleph0_lt_continuum
formalized as: Cardinal.aleph_one_le_iff
formalized as: Cardinal.power_le_power_left

Q193657
formalized as: Convex
formalized as: convexHull
formalized as: ConvexOn
formalized as: convex_iff_add_mem
formalized as: Convex.affine_image
formalized as: Convex.isPathConnected
formalized as: StrictConvex
formalized as: AbsConvex
formalized as: convex_iff_ordConnected
formalized as: Convex.sum_mem
formalized as: Finset.centerMass
formalized as: convex_empty
formalized as: convex_sInter
formalized as: DirectedOn.convex_sUnion
formalized as: IsExtreme
formalized as: Set.extremePoints
formalized as: closure_convexHull_extremePoints
formalized as: StrictConvexSpace.extremePoints_closedBall_eq_sphere
formalized as: Convex.closure
formalized as: Convex.add_smul
formalized as: convexHull_min
formalized as: Set.add
formalized as: Set.addMonoid
formalized as: convexHull_add
formalized as: convexHull_sum
formalized as: convexHullAddMonoidHom
formalized as: IsCompact.add
formalized as: IsClosed.add_left_of_isCompact
formalized as: StarConvex
formalized as: Convex.starConvex
formalized as: Set.OrdConnected
formalized as: Convexity.ConvexSpace

Q66707394
formalized as: Set.Countable
formalized as: Denumerable
formalized as: Function.cantor_surjective
formalized as: countable_iff_exists_injective
formalized as: countable_iff_exists_surjective
formalized as: Uncountable
formalized as: Infinite
formalized as: Equiv
formalized as: Cardinal.eq
formalized as: Cardinal.not_countable_real
formalized as: Cardinal.mk_real
formalized as: Set.Finite.countable
formalized as: Set.countable_infinite_iff_nonempty_denumerable
formalized as: Denumerable.prod
formalized as: Algebraic.countable
formalized as: Subtype.countable
formalized as: Set.Countable.mono
formalized as: Set.Countable.prod
formalized as: Denumerable.int
formalized as: Set.Countable.union
formalized as: Set.countable_iUnion
formalized as: denumerableList
formalized as: Set.countable_setOf_finite_subset
formalized as: Function.Injective.countable
formalized as: Cardinal.cantor
formalized as: IsWellOrder

Q7874246
formalized as: CoxeterMatrix.Group
formalized as: CoxeterSystem
formalized as: CoxeterSystem.simple_mul_simple_self
formalized as: CoxeterMatrix
formalized as: CoxeterSystem.length
formalized as: CoxeterSystem.IsReduced
formalized as: CoxeterSystem.lengthParity

Q190556
formalized as: Complex.cos_add_sin_mul_I_pow
formalized as: Complex.exp_mul_I
formalized as: Complex.cos_three_mul
formalized as: Polynomial.Chebyshev.T_complex_cos

Q1058314
formalized as: Diffeomorph
formalized as: Diffeomorph.toHomeomorph
formalized as: IsLocalDiffeomorph
formalized as: IsImmersion

Q628007
formalized as: shift_eq_sum_fwdDiff_iter
formalized as: Polynomial.fwdDiff_iter_degree_eq_factorial
formalized as: AnalyticAt
formalized as: taylorWithin
formalized as: Lagrange.interpolate

Q149999
formalized as: deriv
formalized as: HasDerivAt
formalized as: deriv_pow
formalized as: hasFDerivAt_iff_isLittleO
formalized as: IsLocalExtr.deriv_eq_zero
formalized as: exists_deriv_eq_zero
formalized as: exists_deriv_eq_slope
formalized as: is_const_of_deriv_eq_zero
formalized as: taylor_mean_remainder_lagrange
formalized as: isLocalMax_of_deriv
formalized as: isLocalMin_of_deriv_deriv_pos
formalized as: IsLocalExtr.fderiv_eq_zero
formalized as: ImplicitFunctionData.implicitFunction
formalized as: HasStrictFDerivAt.to_localInverse

Q11214
formalized as: HarmonicAt

Q188444
formalized as: IsRiemannianManifold
formalized as: LieGroup
formalized as: GroupLieAlgebra

Q2502381
formalized as: ContDiffOn
formalized as: EuclideanSpace.instIsManifoldSphere
formalized as: VectorField.mlieBracket
formalized as: RiemannianMetric
formalized as: pathELength_comp_of_monotoneOn
formalized as: EuclideanGeometry.law_cos

Q272621
formalized as: Representation

Q1195339
formalized as: SimpleGraph.hasse
formalized as: Quiver.Arborescence

Q20968946
formalized as: slope
formalized as: BoxIntegral.integralSum
formalized as: intervalIntegral.integral_eq_sub_of_hasDerivAt
formalized as: Finset.sum_range_sub
formalized as: fwdDiff
formalized as: fwdDiff_const
formalized as: fwdDiff_add
formalized as: fwdDiff_smul
formalized as: Geometry.SimplicialComplex
formalized as: AlgebraicTopology.AlternatingFaceMapComplex.objD
formalized as: HomologicalComplex.cycles
formalized as: HomologicalComplex.d_comp_d
formalized as: ChainComplex
formalized as: HomologicalComplex.Hom
formalized as: CochainComplex
formalized as: groupCohomology.cocycles

Q121416
formalized as: peirce

Q865811
formalized as: Distribution
formalized as: TestFunction
formalized as: Distribution.delta
formalized as: TemperedDistribution.toTemperedDistribution_dirac_eq_delta
formalized as: Distribution.lineDerivCLM
formalized as: HasCompactSupport
formalized as: MeasureTheory.LocallyIntegrable
formalized as: ae_eq_of_integral_contDiff_smul_eq
formalized as: LineDeriv.iteratedLineDerivOp
formalized as: Distribution.IsVanishingOn
formalized as: Distribution.dsupport
formalized as: TemperedDistribution
formalized as: SchwartzMap
formalized as: SchwartzMap.seminorm
formalized as: SchwartzMap.fourierTransformCLM
formalized as: TemperedDistribution.derivCLM
formalized as: Function.HasTemperateGrowth.toTemperedDistribution
formalized as: TemperedDistribution.instFourierTransform
formalized as: FourierTransform.fourierCLE

Q752487
formalized as: Module.Dual
formalized as: StrongDual
formalized as: Module.Dual.eval
formalized as: Basis.dualBasis
formalized as: Basis.dualBasis_apply_self
formalized as: Module.lift_rank_lt_rank_dual
formalized as: Module.rank_dual_eq_card_dual_of_aleph0_le_rank
formalized as: LinearMap.BilinForm.toDual
formalized as: Module.evalEquiv
formalized as: LinearMap.dualMap
formalized as: Module.Dual.transpose_apply
formalized as: LinearMap.toMatrix_transpose
formalized as: Submodule.dualAnnihilator
formalized as: Submodule.dualAnnihilator_sup_eq
formalized as: Module.dualAnnihilator_gc
formalized as: Submodule.dualQuotEquivDualAnnihilator
formalized as: Module.dualProdDualEquivDual
formalized as: LinearMap.toContinuousLinearMap
formalized as: ContinuousLinearMap.toNormedAddCommGroup
formalized as: WeakDual
formalized as: InnerProductSpace.toDual
formalized as: RealRMK.integral_rieszMeasure
formalized as: NormedSpace.inclusionInDoubleDual
formalized as: NormedSpace.inclusionInDoubleDualLi

Q211294
formalized as: pow_zero
formalized as: add_comm
formalized as: left_distrib
formalized as: EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two
formalized as: mul_lt_mul_of_neg_left
formalized as: eq_equivalence
formalized as: Eq.subst
formalized as: lt_trans
formalized as: ge_iff_le
formalized as: mul_eq_zero
formalized as: quadratic_eq_zero_iff
formalized as: Real.rpow_inv_natCast_pow

Q268493
formalized as: WeierstrassCurve.Affine.Nonsingular
formalized as: WeierstrassCurve.IsShortNF
formalized as: WeierstrassCurve.Affine.Point.instAddCommGroup
formalized as: WeierstrassCurve.Affine.Point.neg
formalized as: WeierstrassCurve.Affine.Point.add
formalized as: WeierstrassCurve.Affine.Point
formalized as: WeierstrassCurve.Affine.Point.map
formalized as: WeierstrassCurve.Affine.slope_of_X_ne
formalized as: WeierstrassCurve.Affine.negY
formalized as: WeierstrassCurve.Affine.slope_of_Y_ne
formalized as: WeierstrassCurve.Affine.slope
formalized as: WeierstrassCurve.LFunction
formalized as: WeierstrassCurve.exists_variableChange_isShortNF
formalized as: WeierstrassCurve.exists_variableChange_isCharThreeNF
formalized as: WeierstrassCurve.exists_variableChange_isCharTwoNF
formalized as: PeriodPair.derivWeierstrassP_sq
formalized as: PeriodPair.weierstrassP_add_coe
formalized as: WeierstrassCurve.exists_variableChange_of_j_eq
formalized as: PeriodPair.g₂

Q1332450
formalized as: Projectivization.equivSubmodule

Q842346
formalized as: Eq
formalized as: Ne
formalized as: Eq.refl
formalized as: Eq.symm
formalized as: Eq.trans
formalized as: Eq.subst
formalized as: congrArg
formalized as: BEq
formalized as: funext
formalized as: rfl
formalized as: Set.ext
formalized as: setOf
formalized as: Set.ext_iff
formalized as: Prod.ext_iff
formalized as: FP.Float
formalized as: Equivalence
formalized as: Setoid.isPartition_classes
formalized as: Setoid.bot_def
formalized as: Con
formalized as: CategoryTheory.Iso
formalized as: Equiv
formalized as: MulEquiv
formalized as: zmodMulEquivOfGenerator
formalized as: LinearEquiv.nonempty_equiv_iff_rank_eq
formalized as: EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two
formalized as: EuclideanSpace.volume_ball
formalized as: Similar

Q230848
formalized as: EuclideanDomain.gcd
formalized as: Nat.gcd_sub_self_left
formalized as: Int.gcd_eq_gcd_ab
formalized as: Nat.gcd
formalized as: Nat.Coprime
formalized as: Nat.dvd_gcd
formalized as: Nat.factorization_gcd
formalized as: Int.gcd_least_linear
formalized as: Nat.gcd_rec
formalized as: Nat.gcd_comm
formalized as: EuclideanDomain.div_add_mod
formalized as: Int.ediv_emod_unique
formalized as: Nat.xgcd
formalized as: EuclideanDomain.gcd_eq_gcd_ab
formalized as: span_gcd
formalized as: IsPrincipalIdealRing
formalized as: Nat.gcd_eq_gcd_ab
formalized as: Nat.Prime.dvd_mul
formalized as: Nat.Coprime.mul_right
formalized as: Nat.factorization_inj
formalized as: Int.gcd_dvd_iff
formalized as: ZMod.instField
formalized as: ZMod.unitOfCoprime
formalized as: ZMod.chineseRemainder
formalized as: EuclideanDomain
formalized as: GenContFract.terminates_iff_rat
formalized as: Polynomial.instEuclideanDomain
formalized as: EuclideanDomain.gcd_dvd_left
formalized as: GaussianInt
formalized as: PrincipalIdealRing.to_uniqueFactorizationMonoid
formalized as: Zsqrtd.norm
formalized as: EuclideanDomain.to_principal_ideal_domain
formalized as: Zsqrtd
formalized as: Nat.sum_four_squares

Q162886
formalized as: EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two
formalized as: Nat.exists_infinite_primes
formalized as: EuclideanGeometry.angle_eq_angle_of_dist_eq
formalized as: EuclideanGeometry.angle_add_angle_add_angle_eq_pi
formalized as: EuclideanGeometry.angle_eq_pi_div_two_iff_mem_sphere_of_isDiameter
formalized as: EuclideanGeometry.side_side_side
formalized as: EuclideanGeometry.similar_of_angle_angle
formalized as: MeasureTheory.Measure.addHaar_smul
formalized as: Congruent
formalized as: Similar
formalized as: EuclideanSpace.dist_eq
formalized as: and_not_self_iff
formalized as: em

Q168698
formalized as: Real.exp
formalized as: Real.exp_add
formalized as: Real.tendsto_exp_div_pow_atTop
formalized as: Real.exp_pos
formalized as: Real.hasDerivAt_exp
formalized as: Real.exp_log
formalized as: Complex.exp
formalized as: Complex.isCauSeq_norm_exp
formalized as: Real.tendsto_one_add_div_pow_exp
formalized as: Real.exp_neg
formalized as: Real.exp_strictMono
formalized as: Real.rpow
formalized as: Complex.analyticOnNhd_cexp
formalized as: Complex.tendsto_one_add_div_pow_exp
formalized as: Complex.exp_add
formalized as: Complex.exp_log
formalized as: Complex.exp_periodic
formalized as: Complex.exp_conj
formalized as: Complex.norm_exp
formalized as: Complex.exp_mul_I
formalized as: Complex.exp_eq_exp_re_mul_sin_add_cos
formalized as: Complex.two_cos
formalized as: NormedSpace.exp
formalized as: NormedSpace.isUnit_exp

Q5446431
formalized as: CategoryTheory.Functor.Fiber
formalized as: CategoryTheory.Functor.IsStronglyCartesian
formalized as: CategoryTheory.Functor.IsPreFibered.pullbackObj
formalized as: CategoryTheory.Functor.IsStronglyCartesian.isIso_of_base_isIso
formalized as: CategoryTheory.Functor.IsCartesian.domainUniqueUpToIso
formalized as: CategoryTheory.BasedCategory
formalized as: CategoryTheory.BasedCategory.bicategory
formalized as: CategoryTheory.Functor.IsFibered
formalized as: CategoryTheory.Pseudofunctor.CoGrothendieck.forget
formalized as: CategoryTheory.Functor.IsStronglyCocartesian

Q4055684
formalized as: FirstOrder.Language
formalized as: FirstOrder.Language.Theory
formalized as: FirstOrder.Language.Structure
formalized as: FirstOrder.Language.Term
formalized as: FirstOrder.Language.Relations
formalized as: FirstOrder.Language.Functions
formalized as: FirstOrder.Language.Constants
formalized as: FirstOrder.Language.BoundedFormula
formalized as: FirstOrder.Language.BoundedFormula.IsAtomic
formalized as: FirstOrder.Language.BoundedFormula.freeVarFinset
formalized as: FirstOrder.Language.Sentence
formalized as: FirstOrder.Language.BoundedFormula.Realize
formalized as: FirstOrder.Language.Theory.IsSatisfiable
formalized as: FirstOrder.Language.Theory.ModelsBoundedFormula
formalized as: FirstOrder.Language.Theory.Model
formalized as: FirstOrder.Language.Term.bdEqual
formalized as: FirstOrder.Language.exists_elementarySubstructure_card_eq
formalized as: FirstOrder.Language.Theory.isSatisfiable_iff_isFinitelySatisfiable
formalized as: FirstOrder.Language.Theory.exists_model_card_eq
formalized as: ExistsUnique

Q976981
formalized as: EuclideanSpace.volume_ball
formalized as: FirstOrder.Language.BoundedFormula

Q184410
formalized as: SimpleGraph.degree
formalized as: SimpleGraph.nonempty_hom_of_forall_finite_subgraph_hom

Q1365258
formalized as: MeasureTheory.Integrable.fourier_inversion
formalized as: VectorFourier.fourierIntegral
formalized as: MeasureTheory.Lp.fourierTransformₗᵢ
formalized as: hasDerivAt_exp
formalized as: Real.fourier_mul_convolution_eq
formalized as: Real.fourierIntegral
formalized as: Real.fourierIntegralInv
formalized as: AddCircle.hasSum_fourier_series_of_summable
formalized as: Real.tsum_eq_tsum_fourier_of_rpow_decay
formalized as: ZMod.dft
formalized as: ZMod.invDFT_def

Q81392
formalized as: MeasureTheory.dimH
formalized as: NowhereDifferentiable.exists_uniformContinuous_and_not_differentiableAt
formalized as: cantorSet

Q864475
formalized as: CategoryTheory.Functor
formalized as: CategoryTheory.Functor.op
formalized as: CategoryTheory.prod
formalized as: CategoryTheory.Functor.map_isIso
formalized as: CategoryTheory.Functor.comp
formalized as: CategoryTheory.SingleObj
formalized as: TopCat.Presheaf
formalized as: CategoryTheory.Functor.const
formalized as: CategoryTheory.Functor.id
formalized as: CategoryTheory.Functor.diag
formalized as: CategoryTheory.Limits.lim
formalized as: CategoryTheory.MonoidalCategory.tensor
formalized as: CategoryTheory.forget
formalized as: MonCat.free
formalized as: CategoryTheory.Functor.hom
formalized as: CategoryTheory.Functor.IsRepresentable
formalized as: CategoryTheory.Functor.category

Q44455
formalized as: Sion.exists_isSaddlePointOn

Q621550
formalized as: TopologicalSpace
formalized as: IsOpen
formalized as: TopologicalSpace.IsTopologicalBasis
formalized as: instTopologicalSpaceSubtype
formalized as: instTopologicalSpaceProd
formalized as: TopologicalSpace.coinduced
formalized as: DiscreteTopology
formalized as: IndiscreteTopology
formalized as: CofiniteTopology
formalized as: Real.pseudoMetricSpace
formalized as: PseudoMetricSpace
formalized as: PrimeSpectrum.zariskiTopology
formalized as: sierpinskiSpace
formalized as: OrderTopology
formalized as: ContinuousAt
formalized as: continuous_of_discreteTopology
formalized as: continuousAt_def
formalized as: Continuous.tendsto
formalized as: SeqContinuous
formalized as: Continuous.seqContinuous
formalized as: continuous_iff_seqContinuous
formalized as: continuous_iff_continuousAt
formalized as: closure
formalized as: continuous_iff_image_closure_subset_closure_image
formalized as: Continuous.comp
formalized as: IsCompact.image
formalized as: IsConnected.image
formalized as: IsPathConnected.image
formalized as: IsLindelof.image
formalized as: ContinuousOn.isSeparable_image
formalized as: TopologicalSpace.le_def
formalized as: continuous_id_iff_le
formalized as: IsOpenMap
formalized as: Homeomorph
formalized as: Continuous.homeoOfEquivCompactToT2
formalized as: TopologicalSpace.induced
formalized as: CompactSpace
formalized as: IsCompact
formalized as: isCompact_Icc
formalized as: isCompact_iff_isClosed_bounded
formalized as: IsCompact.isClosed
formalized as: IsCompact.tendsto_subseq
formalized as: exists_embedding_euclidean_of_compact
formalized as: ConnectedSpace
formalized as: isPreconnected_iff_subset_of_disjoint
formalized as: isPreconnected_Icc
formalized as: IsPreconnected.image
formalized as: connectedComponent
formalized as: connectedComponentSetoid
formalized as: TotallyDisconnectedSpace
formalized as: TotallySeparatedSpace
formalized as: TotallySeparatedSpace.totallyDisconnectedSpace
formalized as: Path
formalized as: pathComponent
formalized as: PathConnectedSpace
formalized as: PathConnectedSpace.connectedSpace
formalized as: Pi.topologicalSpace
formalized as: IsTopologicalBasis.prod
formalized as: isCompact_pi_infinite
formalized as: T0Space
formalized as: T1Space
formalized as: T2Space
formalized as: T25Space
formalized as: RegularSpace
formalized as: CompletelyRegularSpace
formalized as: NormalSpace
formalized as: exists_continuous_zero_one_of_isClosed
formalized as: CompletelyNormalSpace
formalized as: PerfectlyNormalSpace
formalized as: ContinuousMap.exists_restrict_eq
formalized as: SequentialSpace
formalized as: FirstCountableTopology
formalized as: SecondCountableTopology
formalized as: SeparableSpace
formalized as: LindelofSpace
formalized as: SigmaCompactSpace
formalized as: FirstCountableTopology.frechetUrysohnSpace
formalized as: SecondCountableTopology.to_firstCountableTopology
formalized as: IsSigmaCompact.isLindelof
formalized as: UniformSpace.firstCountableTopology

Q213488
formalized as: Manifold.pathELength
formalized as: Manifold.riemannianEDist

Q2662474
formalized as: SimpleGraph.mulCayley
formalized as: Int.instAddCommGroup
formalized as: FreeGroup
formalized as: Monoid.CoprodI
formalized as: Equiv.Perm
formalized as: CoxeterSystem

Q8087
formalized as: ChartedSpace
formalized as: IsManifold
formalized as: InnerProductGeometry.angle
formalized as: EuclideanGeometry.angle
formalized as: EuclideanSpace.dist_eq
formalized as: MetricSpace
formalized as: MeasureTheory.Measure
formalized as: Similar
formalized as: MvPolynomial.vanishingIdeal_zeroLocus_eq_radical
formalized as: Convex

Q200787
formalized as: FirstOrder.Language.Theory.IsComplete
formalized as: FirstOrder.Field.ACF_isComplete
formalized as: Nat.Partrec.Code.halting_problem

Q504843
formalized as: SimpleGraph.Coloring
formalized as: SimpleGraph.Colorable
formalized as: SimpleGraph.chromaticNumber
formalized as: SimpleGraph.chromaticNumber_eq_iff_colorable_not_colorable
formalized as: SimpleGraph.Coloring.colorClass
formalized as: SimpleGraph.partitionable_iff_colorable
formalized as: SimpleGraph.chromaticNumber_le_card
formalized as: SimpleGraph.chromaticNumber_eq_one_iff
formalized as: SimpleGraph.chromaticNumber_top
formalized as: SimpleGraph.isBipartite_iff_exists_isBipartiteWith
formalized as: SimpleGraph.IsClique.card_le_chromaticNumber
formalized as: SimpleGraph.nonempty_hom_of_forall_finite_subgraph_hom

Q131476
formalized as: SimpleGraph
formalized as: Quiver
formalized as: Graph
formalized as: SimpleGraph.Coloring
formalized as: SimpleGraph.isTuranMaximal_iff_nonempty_iso_turanGraph
formalized as: SimpleGraph.szemeredi_regularity
formalized as: SimpleGraph.IsTree
formalized as: SimpleGraph.incMatrix
formalized as: SimpleGraph.adjMatrix
formalized as: SimpleGraph.degMatrix
formalized as: SimpleGraph.lapMatrix

Q131752
formalized as: GCDMonoid.gcd
formalized as: Nat.gcd
formalized as: Int.gcd
formalized as: EuclideanDomain.gcd_zero_right
formalized as: gcd_eq_zero_iff
formalized as: dvd_gcd_iff
formalized as: Nat.Coprime
formalized as: Nat.gcd_mul_lcm
formalized as: Nat.factorization_gcd
formalized as: Nat.gcd_sub_self_left
formalized as: EuclideanDomain.gcd_val
formalized as: EuclideanDomain.gcd_self
formalized as: Int.gcd_eq_gcd_ab
formalized as: IsCoprime.dvd_of_dvd_mul_right
formalized as: Nat.gcd_mul_left
formalized as: Nat.gcd_add_mul_right_left
formalized as: Nat.gcd_div
formalized as: Nat.coprime_div_gcd_div_gcd
formalized as: gcd_comm
formalized as: gcd_assoc
formalized as: Nat.Coprime.gcd_mul
formalized as: gcd_mul_lcm
formalized as: Nat.totient_gcd_mul_totient_mul
formalized as: GCDMonoid
formalized as: UniqueFactorizationMonoid.toGCDMonoid
formalized as: EuclideanDomain.gcd
formalized as: span_gcd

Q288465
formalized as: MulAction
formalized as: Representation
formalized as: Equiv.Perm.applyMulAction
formalized as: FaithfulSMul
formalized as: MulAction.IsPretransitive
formalized as: MulAction.IsMultiplyPretransitive
formalized as: Equiv.Perm.isMultiplyPretransitive
formalized as: MulAction.IsPreprimitive
formalized as: ProperlyDiscontinuousSMul
formalized as: ContinuousSMul
formalized as: ProperSMul
formalized as: IsSemisimpleRepresentation
formalized as: MulAction.orbit
formalized as: MulAction.orbitRel
formalized as: MulAction.pretransitive_iff_subsingleton_quotient
formalized as: MulAction.orbitRel.Quotient
formalized as: MulAction.IsInvariantBlock
formalized as: MulAction.IsFixedBlock.orbit
formalized as: MulAction.fixedPoints
formalized as: MulAction.fixedBy
formalized as: MulAction.stabilizer
formalized as: MulAction.stabilizer_smul_eq_stabilizer_map_conj
formalized as: MulAction.orbitEquivQuotientStabilizer
formalized as: MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group
formalized as: Monoid.toMulAction
formalized as: MulAction.quotient
formalized as: ConjAct
formalized as: Units.instMulAction
formalized as: LinearEquiv.applyDistribMulAction
formalized as: CategoryTheory.Action
formalized as: AlgEquiv.applyMulSemiringAction
formalized as: Flow
formalized as: Set.mulAction
formalized as: CategoryTheory.ActionCategory
formalized as: MulActionHom
formalized as: CategoryTheory.actionAsFunctor

Q1055807
formalized as: Action.ρAut
formalized as: Representation
formalized as: Action.IsContinuous
formalized as: MonoidHom.ker
formalized as: Representation.IntertwiningMap
formalized as: Representation.Equiv
formalized as: Subrepresentation
formalized as: Representation.IsIrreducible
formalized as: Representation.IsSemisimpleRepresentation
formalized as: MulAction
formalized as: MulAction.bijective
formalized as: Action.functorCategoryEquivalence
formalized as: Rep

Q326908
formalized as: SeparatedNhds
formalized as: T2Space
formalized as: R1Space
formalized as: R1Space.t2Space_iff_t0Space
formalized as: SeparationQuotient.t2Space_iff
formalized as: t2_iff_isClosed_diagonal
formalized as: t2Space_of_metrizableSpace
formalized as: CofiniteTopology.instT1Space
formalized as: PseudoMetrizableSpace.regularSpace
formalized as: Prod.t2Space
formalized as: T2Space.t1Space
formalized as: R1Space.instR0Space
formalized as: R1Space.quasiSober
formalized as: IsCompact.isClosed
formalized as: SeparatedNhds.of_isCompact_isCompact
formalized as: NormalSpace.of_compactSpace_r1Space
formalized as: t2Space_iff_of_isOpenQuotientMap
formalized as: isClosed_eq
formalized as: Continuous.ext_on
formalized as: T2Space.r1Space
formalized as: CompleteSpace
formalized as: ContinuousMap.instCommCStarAlgebra

Q273167
formalized as: MeasureTheory.IsProbabilityMeasure
formalized as: RiemannHypothesis

Q5018842
formalized as: left_distrib
formalized as: mul_comm
formalized as: mul_self_sub_mul_self
formalized as: add_sq
formalized as: Nat.chineseRemainder
formalized as: Polynomial
formalized as: sq_add_sq_mul
formalized as: quadratic_eq_zero_iff
formalized as: PythagoreanTriple
formalized as: Pell.IsFundamental.eq_zpow_or_neg_zpow
formalized as: quadratic_ne_zero_of_discrim_ne_sq
formalized as: Matrix.det
formalized as: Complex.exists_root
formalized as: isSolvable_gal_of_irreducible
formalized as: intermediateFieldEquivSubgroup

Q2393733
formalized as: EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two

Q3893386
formalized as: InnerProductGeometry.norm_add_sq_eq_norm_sq_add_norm_sq'
formalized as: Nat.Prime.dvd_mul
formalized as: Nat.fib
formalized as: Matrix.cramer
formalized as: Field
formalized as: Cardinal.aleph

Q185264
formalized as: norm_add_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two
formalized as: Nat.Perfect
formalized as: quadratic_eq_zero_iff
formalized as: EuclideanGeometry.thales_theorem
formalized as: irrational_sqrt_two
formalized as: Nat.exists_infinite_primes
formalized as: EuclideanGeometry.mul_dist_add_mul_dist_eq_mul_dist_of_cospherical
formalized as: Nat.choose_succ_succ
formalized as: add_pow
formalized as: Nat.fib
formalized as: Real.sin
formalized as: Zsqrtd.norm_mul
formalized as: exists_hasDerivAt_eq_slope
formalized as: Pell.exists_of_not_isSquare
formalized as: Real.tendsto_sum_pi_div_four
formalized as: Real.hasSum_arctan
formalized as: Real.hasSum_cos
formalized as: Real.cos_eq_tsum
formalized as: Complex
formalized as: Complex.I
formalized as: Complex.exists_root
formalized as: legendreSym.quadratic_reciprocity
formalized as: ChartedSpace
formalized as: Module
formalized as: Quaternion
formalized as: BooleanAlgebra
formalized as: isSolvable_gal_of_irreducible
formalized as: ZFSet
formalized as: Padic
formalized as: MeasureTheory.IsProbabilityMeasure
formalized as: MeasureTheory.lintegral
formalized as: Hyperreal
formalized as: LucasLehmer.lucas_lehmer_sufficiency

Q5870804
formalized as: Differentiable
formalized as: Continuous
formalized as: BooleanRing
formalized as: Classical.epsilon
formalized as: Partrec
formalized as: halting_problem
formalized as: ZFSet.sep
formalized as: ZFSet.pair

Q5887297
formalized as: CategoryTheory.LocallySmall
formalized as: CategoryTheory.coyoneda
formalized as: CategoryTheory.yoneda
formalized as: CategoryTheory.Functor.hom
formalized as: CategoryTheory.yonedaEquiv
formalized as: CategoryTheory.MonoidalClosed.internalHom
formalized as: CategoryTheory.MonoidalClosed
formalized as: CategoryTheory.ihom.adjunction
formalized as: CategoryTheory.ihom
formalized as: CategoryTheory.Functor.IsRepresentable
formalized as: CategoryTheory.Profunctor.id
formalized as: CategoryTheory.Adjunction.rightAdjoint_preservesLimits
formalized as: CategoryTheory.projective_iff_preservesEpimorphisms_coyoneda_obj
formalized as: TensorProduct.lift.equiv

Q579978
formalized as: ChainComplex
formalized as: HomologicalComplex.d
formalized as: HomologicalComplex.homology
formalized as: HomologicalComplex.Acyclic
formalized as: singularChainComplexFunctor
formalized as: CategoryTheory.ShortComplex.Exact
formalized as: CategoryTheory.ShortComplex.ShortExact
formalized as: CategoryTheory.Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono
formalized as: CategoryTheory.ShortComplex.SnakeInput.snake_lemma
formalized as: CategoryTheory.Abelian
formalized as: CategoryTheory.Functor.rightDerived
formalized as: Ext
formalized as: CategoryTheory.Tor
formalized as: CategoryTheory.SpectralSequence
formalized as: singularHomologyFunctor
formalized as: HomologicalComplex.Hom
formalized as: HomologicalComplex.QuasiIso
formalized as: HomologicalComplex.homologyFunctor
formalized as: CategoryTheory.ShortComplex.ShortExact.δ

Q215111
formalized as: map_one
formalized as: MulHom
formalized as: MonoidHom
formalized as: RingHom
formalized as: NonUnitalRingHom
formalized as: LinearMap
formalized as: AlgHom
formalized as: Matrix.scalar
formalized as: MulEquiv
formalized as: CategoryTheory.Iso
formalized as: EquivLike.bijective
formalized as: MulEquiv.ofBijective
formalized as: Homeomorph
formalized as: Monoid.End
formalized as: Monoid.End.instMonoid
formalized as: Module.End.instRing
formalized as: MulAut
formalized as: LinearMap.GeneralLinearGroup
formalized as: CategoryTheory.mono_iff_injective
formalized as: CategoryTheory.Mono
formalized as: CategoryTheory.SplitMono
formalized as: CategoryTheory.IsSplitMono.mono
formalized as: CategoryTheory.ConcreteCategory.mono_of_injective
formalized as: CategoryTheory.epi_iff_surjective
formalized as: CategoryTheory.Epi
formalized as: IsLocalization.epi
formalized as: CategoryTheory.SplitEpi
formalized as: CategoryTheory.SplitEpi.epi
formalized as: Con.ker
formalized as: Con.quotientKerEquivRange
formalized as: QuotientGroup.con_ker_eq_conKer
formalized as: FirstOrder.Language.Hom
formalized as: SimpleGraph.Hom

Q1279571
formalized as: EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two
formalized as: PythagoreanTriple
formalized as: Nat.choose_succ_succ
formalized as: Nat.sum_range_choose
formalized as: Nat.factorial
formalized as: Real.sin
formalized as: Real.pi_gt_d4
formalized as: Real.sin_sq_add_cos_sq
formalized as: mul_zero
formalized as: quadratic_eq_zero_iff
formalized as: sq_add_mul_sq_mul_sq_add_mul_sq
formalized as: Real.deriv_sin
formalized as: exists_deriv_eq_zero
formalized as: Real.pi_gt_d6
formalized as: mul_self_eq_mul_self_iff
formalized as: Real.sin_add
formalized as: Real.hasSum_sin
formalized as: tsum_geometric_of_lt_one
formalized as: Real.hasSum_arctan
formalized as: Real.tendsto_sum_pi_div_four
formalized as: exists_hasDerivAt_eq_slope

Q131222
formalized as: Real.negMulLog_zero
formalized as: Real.binEntropy
formalized as: Real.binEntropy_le_log_two
formalized as: InformationTheory.klDiv

Q12503
formalized as: Int
formalized as: Denumerable.int
formalized as: Int.instCommRing
formalized as: Int.instAddCommGroup
formalized as: CommRingCat.zIsInitial
formalized as: RingHom.injective_int
formalized as: instIsAddCyclicInt
formalized as: intCyclicAddEquiv
formalized as: Int.instCommMonoid
formalized as: Int.instIsDomain
formalized as: Int.not_isField
formalized as: Rat.isFractionRing
formalized as: Int.ediv_emod_unique''
formalized as: Int.euclideanDomain
formalized as: Nat.primeFactorsList_unique
formalized as: Int.instLinearOrder
formalized as: Int.instIsStrictOrderedRing
formalized as: sub_eq_add_neg
formalized as: Equiv.intEquivNat
formalized as: Cardinal.mk_int
formalized as: Function.Bijective

Q187631
formalized as: AffineMap.lineMap
formalized as: AffineMap.lineMap_apply_ring
formalized as: Lagrange.interpolate
formalized as: Lagrange.eq_interpolate_iff

Q16743426
formalized as: Circle.instCommGroup
formalized as: CommGroup
formalized as: Group
formalized as: Int.instAddCommGroup

Q838495
formalized as: Module.End.genEigenspace
formalized as: Module.End.maxGenEigenspaceIndex
formalized as: Module.End.exists_isNilpotent_isSemisimple
formalized as: spectrum.map_polynomial_aeval_of_degree_pos
formalized as: Matrix.charpoly_units_conj
formalized as: LinearMap.aeval_self_charpoly
formalized as: minpoly
formalized as: IsCompactOperator.hasEigenvalue_iff_mem_spectrum

Q1765138
formalized as: tsum_geometric_of_lt_one
formalized as: Real.hasSum_sin
formalized as: Real.hasSum_cos
formalized as: Real.tendsto_sum_pi_div_four
formalized as: Real.deriv_sin

Q11476
formalized as: Isometry
formalized as: Matrix.mem_orthogonalGroup_iff'

Q1225713
formalized as: ringKrullDim
formalized as: ringKrullDim_eq_zero_of_field
formalized as: Ring.krullDimLE_zero_and_isLocalRing_tfae
formalized as: RelSeries.length
formalized as: Ideal.primeHeight
formalized as: Ideal.primeHeight_eq_zero_iff
formalized as: Ideal.sup_primeHeight_of_maximal_eq_ringKrullDim
formalized as: Ideal.finiteHeight_of_isNoetherianRing
formalized as: Ideal.height_le_iff_exists_minimalPrimes
formalized as: Ideal.height
formalized as: PrimeSpectrum.topologicalKrullDim_eq_ringKrullDim
formalized as: MvPolynomial.ringKrullDim_of_isNoetherianRing
formalized as: Polynomial.ringKrullDim_of_isNoetherianRing
formalized as: IsPrincipalIdealRing.ringKrullDim_eq_one
formalized as: Ring.KrullDimLE.isField_of_isDomain
formalized as: ringKrullDim_eq_bot_of_subsingleton
formalized as: ringKrullDim_nonneg_of_nontrivial
formalized as: isArtinianRing_iff_isNoetherianRing_krullDimLE_zero
formalized as: Module.supportDim

Q199691
formalized as: ProbabilityTheory.mgf

Q484637
formalized as: AffineMap

Q202843
formalized as: IsMinOn.of_isLocalMin_of_convex_univ

Q8078
formalized as: em
formalized as: inf_sup_left

Q1166618
formalized as: Metric.continuousAt_iff
formalized as: Cardinal.not_countable_real
formalized as: Function.cantor_surjective
formalized as: exists_wellFoundedLT
formalized as: ZFSet.isOrdinal_notMem_univ
formalized as: FirstOrder.Language.exists_elementarySubstructure_card_eq
formalized as: FirstOrder.Language.Theory.isSatisfiable_iff_isFinitelySatisfiable
formalized as: FirstOrder.Language
formalized as: ZFSet
formalized as: Classical.axiomOfChoice
formalized as: FirstOrder.Language.Theory
formalized as: ComputablePred.halting_problem

Q141495
formalized as: IsMinOn
formalized as: IsLocalMin
formalized as: IsMinOn.of_isLocalMin_of_convex_univ
formalized as: IsCompact.exists_isMinOn
formalized as: LowerSemicontinuousOn.exists_isMinOn
formalized as: IsLocalExtr.hasDerivAt_eq_zero
formalized as: IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt_1d

Q156495
formalized as: intervalIntegral.integral_eq_sub_of_hasDerivAt
formalized as: IsLocalExtr.deriv_eq_zero
formalized as: fourierCoeff
formalized as: IsRiemannianManifold
formalized as: HilbertSpace
formalized as: spectrum

Q395
formalized as: FermatLastTheorem
formalized as: Module
formalized as: BooleanAlgebra
formalized as: Function.cantor_surjective
formalized as: Module.Flat.of_free
formalized as: Nat.exists_infinite_primes

Q1045555
formalized as: ProbabilityTheory.multivariateGaussian

Q51501
formalized as: gradient
formalized as: hasDerivAt_integral_of_dominated_loc_of_lip

Q2796622
formalized as: Finset.centroid
formalized as: Real.geom_mean_le_arith_mean
formalized as: Finset.affineCombination
formalized as: MeasureTheory.average

Q226995
formalized as: ConvexOn.map_integral_le

Q464794
formalized as: LinearMap.BilinForm.IsOrtho
formalized as: LinearMap.BilinForm.toDual
formalized as: LinearMap.BilinForm.nondegenerate_iff_ker_eq_bot

Q467606
formalized as: FirstOrder.Language.BoundedFormula
formalized as: FirstOrder.Language.Sentence
formalized as: FirstOrder.Language.Theory
formalized as: FirstOrder.Language.Theory.IsSatisfiable
formalized as: FirstOrder.Language.Theory.IsComplete
formalized as: FirstOrder.Language.completeTheory
formalized as: FirstOrder.Language
formalized as: FirstOrder.Language.Structure
formalized as: FirstOrder.Language.Theory.Model
formalized as: FirstOrder.Language.Substructure
formalized as: FirstOrder.Language.ElementarySubstructure
formalized as: FirstOrder.Language.ElementarySubstructure.theory_model_iff
formalized as: FirstOrder.Language.ElementaryEmbedding
formalized as: FirstOrder.Language.Embedding.toHom
formalized as: FirstOrder.Language.LHom.reduct
formalized as: FirstOrder.Language.Theory.isSatisfiable_iff_isFinitelySatisfiable
formalized as: FirstOrder.Language.exists_elementarySubstructure_card_eq
formalized as: FirstOrder.Language.Theory.exists_large_model_of_infinite_model
formalized as: Set.Definable
formalized as: FirstOrder.Language.Substructure.isElementary_of_exists
formalized as: Set.DefinableFun
formalized as: FirstOrder.Language.Theory.typeOf
formalized as: FirstOrder.Language.Theory.CompleteType
formalized as: FirstOrder.Language.DefinableSet.instBooleanAlgebra
formalized as: FirstOrder.Language.Theory.CompleteType.instCompactSpace
formalized as: FirstOrder.Language.Ultraproduct.structure
formalized as: FirstOrder.Language.Ultraproduct.sentence_realize
formalized as: Cardinal.Categorical
formalized as: Order.iso_of_countable_dense
formalized as: FirstOrder.Language.IsFraisseLimit

Q18848
formalized as: Module
formalized as: Module.AEval
formalized as: AddCommGroup.uniqueIntModule
formalized as: Module.Free
formalized as: Pi.module
formalized as: Submodule
formalized as: MulOpposite
formalized as: Module.compHom
formalized as: Submodule.span
formalized as: Submodule.instIsModularLattice
formalized as: LinearMap
formalized as: LinearEquiv
formalized as: LinearMap.ker
formalized as: LinearMap.quotKerEquivRange
formalized as: ModuleCat.abelian
formalized as: Module.Finite
formalized as: Module.Projective
formalized as: Module.Injective
formalized as: Module.Flat
formalized as: IsSimpleModule
formalized as: IsSemisimpleModule
formalized as: FaithfulSMul
formalized as: Module.IsTorsionFree
formalized as: IsNoetherian
formalized as: IsArtinian
formalized as: SetLike.GradedSMul
formalized as: Representation
formalized as: Module.toAddMonoidEnd
formalized as: SheafOfModules

Q232207
formalized as: ProbabilityTheory.strong_law_ae

Q190529
formalized as: one_add_one_eq_two
formalized as: Set.empty_def
formalized as: Function.Bijective
formalized as: Metric.ball

Q233858
formalized as: Circle
formalized as: DualNumber

Q617295
formalized as: DFA
formalized as: NFA
formalized as: DFA.toNFA_correct
formalized as: NFA.toDFA_correct
formalized as: NFA.accepts
formalized as: NFA.accepts_iff_exists_path
formalized as: NFA.evalFrom
formalized as: DFA.toNFA
formalized as: εNFA
formalized as: εNFA.εClosure
formalized as: εNFA.evalFrom
formalized as: εNFA.accepts
formalized as: εNFA.toNFA_correct
formalized as: εNFA.toNFA_evalFrom_match
formalized as: Language.IsRegular.add
formalized as: Language.IsRegular.inf
formalized as: Language.IsRegular.compl

Q12479
formalized as: Int
formalized as: PythagoreanTriple
formalized as: Mul
formalized as: Dvd.dvd
formalized as: Nat.div_add_mod
formalized as: Nat.three_dvd_iff
formalized as: Nat.gcd
formalized as: Nat.Coprime
formalized as: EuclideanDomain.gcd
formalized as: GenContFract
formalized as: Nat.Prime
formalized as: Nat.exists_infinite_primes
formalized as: Nat.factorization
formalized as: Nat.primeFactorsList
formalized as: Nat.Prime.dvd_mul
formalized as: Nat.primeFactorsList_unique
formalized as: ZMod
formalized as: Int.ModEq
formalized as: ZMod.pow_card
formalized as: Nat.ModEq.pow_totient
formalized as: Filter.Tendsto
formalized as: Complex.I
formalized as: Complex.re
formalized as: Nat.primeCounting
formalized as: riemannZeta
formalized as: riemannZeta_eulerProduct
formalized as: RiemannHypothesis
formalized as: Ideal.IsPrime
formalized as: dedekindZeta
formalized as: IsAlgebraic
formalized as: NumberField
formalized as: IsAbelianGalois
formalized as: Real.infinite_rat_abs_sub_lt_one_div_den_sq_of_irrational
formalized as: Transcendental

Q11216
formalized as: Lagrange.interpolate
formalized as: IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt

Q82990
formalized as: Nat.ofDigits
formalized as: Nat.ofDigits_eq_sum_mapIdx

Q753445
formalized as: trapezoidal_integral
formalized as: MeasureTheory.integral_prod

Q541182
formalized as: IsPicardLindelof.exists_eq_forall_mem_Icc_hasDerivWithinAt

Q131030
formalized as: Module.End
formalized as: LinearMap
formalized as: LinearMap.toMatrix
formalized as: lp
formalized as: ContinuousLinearMap.toNormedRing
formalized as: ContinuousLinearMap
formalized as: ContinuousLinearMap.addCommGroup
formalized as: gradient
formalized as: LinearMap.GeneralLinearGroup
formalized as: Matrix.orthogonalGroup
formalized as: Matrix.specialOrthogonalGroup
formalized as: VectorFourier.fourierIntegral

Q191780
formalized as: Ordinal
formalized as: InitialSeg.total
formalized as: IsWellOrder
formalized as: Ordinal.type
formalized as: Ordinal.omega0
formalized as: Ordinal.lt_wf
formalized as: OrderIso
formalized as: Ordinal.isEquivalent
formalized as: ZFSet.omega
formalized as: ZFSet.IsOrdinal
formalized as: ZFSet.IsOrdinal.mem
formalized as: ZFSet.IsOrdinal.subset_iff_eq_or_mem
formalized as: Ordinal.bddAbove_of_small
formalized as: Order.lt_succ
formalized as: not_small_ordinal
formalized as: Ordinal.type_eq
formalized as: Ordinal.zero_or_succ_or_isSuccLimit
formalized as: Ordinal.zero_le
formalized as: Order.succ
formalized as: Order.IsSuccLimit
formalized as: Ordinal.isSuccLimit_iff
formalized as: IsSuccPrelimit.sSup_Iio
formalized as: Ordinal.omega0_le_of_isSuccLimit
formalized as: Ordinal.le_iSup
formalized as: Order.IsNormal
formalized as: Ordinal.induction
formalized as: Ordinal.limitRecOn
formalized as: Ordinal.instPow
formalized as: Ordinal.not_bddAbove_fp
formalized as: Ordinal.enumOrd
formalized as: Ordinal.isPrincipal_add_iff_add_lt_ne_self
formalized as: Ordinal.epsilon
formalized as: Ordinal.CNF
formalized as: Cardinal.ord
formalized as: Ordinal.isSuccLimit_ord
formalized as: Ordinal.omega
formalized as: Ordinal.cof
formalized as: Ordinal.cof_eq_aleph0_of_isSuccLimit
formalized as: Ordinal.cof_succ
formalized as: Ordinal.cof_ord_cof
formalized as: IsCofinal
formalized as: Ordinal.IsAcc
formalized as: Ordinal.isClosed_iff_iSup
formalized as: Ordinal.epsilon_zero_eq_nfp
formalized as: derivedSet

Q1783179
formalized as: Matrix.orthogonalGroup
formalized as: Matrix.specialOrthogonalGroup
formalized as: Matrix.mem_orthogonalGroup_iff
formalized as: LinearIsometryEquiv.instGroup
formalized as: AffineIsometryEquiv.instGroup
formalized as: Matrix.det_of_mem_unitary
formalized as: Matrix.mem_specialOrthogonalGroup_iff
formalized as: Submodule.reflection
formalized as: QuadraticForm.equivalent_one_zero_neg_one_weighted_sum_squared
formalized as: QuadraticForm.equivalent_of_isAlgClosed
formalized as: char_dvd_card_solutions_of_sum_lt
formalized as: LieAlgebra.Orthogonal.so
formalized as: LinearIsometry.isConformalMap
formalized as: pinGroup
formalized as: spinGroup

Q333871
formalized as: Matrix.orthogonalGroup
formalized as: Matrix.mem_orthogonalGroup_iff
formalized as: Matrix.specialOrthogonalGroup
formalized as: Matrix.permMatrix_one
formalized as: Equiv.swap
formalized as: Matrix.det_of_mem_unitary
formalized as: Matrix.det_permutation
formalized as: LieAlgebra.Orthogonal.so
formalized as: exp_mem_unitary_of_mem_skewAdjoint
formalized as: Matrix.IsHermitian.spectral_theorem

Q746242
formalized as: ComputablePred.halting_problem

Q48297
formalized as: AffineMap

Q1413083
formalized as: Real.logb
formalized as: Nat.descFactorial
formalized as: circleMap
formalized as: ProbabilityTheory.poissonPMF
formalized as: ProbabilityTheory.gaussianReal

Q1187620
formalized as: SimpleGraph.IsClique
formalized as: SimpleGraph.cliqueNum
formalized as: SimpleGraph.Coloring
formalized as: SimpleGraph.chromaticNumber
formalized as: SimpleGraph.cliqueNum_le_chromaticNumber
formalized as: PartialOrder
formalized as: IncompRel
formalized as: IsChain
formalized as: IsAntichain

Q161519
formalized as: Fintype.card_perm
formalized as: Equiv.Perm
formalized as: Equiv.permGroup
formalized as: Equiv.Perm.one_def
formalized as: Equiv.Perm.cycleFactorsFinset_noncommProd
formalized as: Equiv.Perm.IsCycle
formalized as: Function.IsFixedPt
formalized as: derangements
formalized as: Equiv.swap
formalized as: Equiv.Perm.Disjoint.commute
formalized as: Equiv.Perm.formPerm_reverse
formalized as: Equiv.Perm.mul_apply
formalized as: Equiv.trans
formalized as: Fintype.card_embedding_eq
formalized as: descPochhammer
formalized as: Finset.powersetCard
formalized as: Finset.card_powersetCard
formalized as: Nat.choose
formalized as: Fintype.card_pi_const
formalized as: Equiv.Perm.cycleType
formalized as: Equiv.Perm.card_of_cycleType
formalized as: IsConj
formalized as: Equiv.Perm.isConj_iff_cycleType_eq
formalized as: orderOf
formalized as: Equiv.Perm.lcm_cycleType
formalized as: Equiv.Perm.truncSwapFactors
formalized as: Equiv.Perm.sign
formalized as: Matrix.det_permutation
formalized as: Equiv.Perm.permMatrix
formalized as: Matrix.permMatrixHom

Q530152
formalized as: IsPicardLindelof.exists_eq_forall_mem_Icc_hasDerivWithinAt
formalized as: IsPicardLindelof.picard_eq_of_hasDerivAt
formalized as: ODE.picard
formalized as: ContractingWith.tendsto_iterate_fixedPoint
formalized as: ContractingWith.exists_fixedPoint
formalized as: IsPicardLindelof.FunSpace.exists_contractingWith_iterate_next
formalized as: IsPicardLindelof.FunSpace.dist_iterate_next_apply_le
formalized as: ContractingWith.isFixedPt_fixedPoint_iterate
formalized as: ContDiffAt.exists_forall_mem_closedBall_exists_eq_forall_mem_Ioo_hasDerivAt

Q188276
formalized as: Fintype.exists_ne_map_eq_of_card_lt
formalized as: Fintype.exists_lt_card_fiber_of_mul_lt_card
formalized as: Function.Embedding.isEmpty_of_card_lt
formalized as: AddCircle.denseRange_zsmul_coe_iff
formalized as: Finite.exists_ne_map_eq_of_infinite
formalized as: Fintype.exists_card_fiber_le_of_card_le_mul
formalized as: Finset.exists_ne_map_eq_of_card_lt_of_maps_to
formalized as: Fintype.card_le_of_injective
formalized as: Fintype.card_le_of_surjective
formalized as: Fintype.exists_le_card_fiber_of_mul_le_card
formalized as: Fintype.exists_card_fiber_lt_of_card_lt_mul
formalized as: Cardinal.le_def
formalized as: Cardinal.exists_uncountable_fiber
formalized as: Cardinal.infinite_pigeonhole

Q205692
formalized as: poissonMeasure
formalized as: poissonMeasure_singleton
formalized as: tendsto_choose_mul_pow_of_tendsto_mul_atTop

Q206925
formalized as: FormalMultilinearSeries
formalized as: Polynomial.taylor
formalized as: tsum_geometric_of_norm_lt_one
formalized as: NormedSpace.exp_eq_tsum
formalized as: Real.sin_eq_tsum
formalized as: FormalMultilinearSeries.radius
formalized as: FormalMultilinearSeries.radius_inv_eq_limsup
formalized as: FormalMultilinearSeries.ofScalars_radius_eq_inv_of_tendsto
formalized as: FormalMultilinearSeries.summable_norm_apply
formalized as: Real.tendsto_tsum_powerSeries_nhdsWithin_lt
formalized as: HasFPowerSeriesOnBall.add
formalized as: FormalMultilinearSeries.min_radius_le_radius_add
formalized as: AnalyticAt.mul
formalized as: tsum_mul_tsum_eq_tsum_sum_antidiagonal
formalized as: PowerSeries.inv
formalized as: HasFPowerSeriesOnBall.fderiv
formalized as: AnalyticAt
formalized as: FormalMultilinearSeries.analyticOnNhd
formalized as: DifferentiableOn.analyticAt
formalized as: AnalyticAt.contDiffAt
formalized as: HasFPowerSeriesOnBall.factorial_smul
formalized as: HasFPowerSeriesOnBall.hasSum_iteratedFDeriv
formalized as: AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq
formalized as: PowerSeries.mk
formalized as: FormalMultilinearSeries.hasFPowerSeriesOnBall
formalized as: PowerSeries
formalized as: MvPowerSeries
formalized as: PowerSeries.order

Q915906
formalized as: PresentedGroup
formalized as: FreeGroup
formalized as: Group.IsFinitelyPresented

Q863912
formalized as: Ideal.IsPrime
formalized as: Ideal.span_singleton_prime
formalized as: Nat.Prime.dvd_mul
formalized as: PrimeSpectrum
formalized as: AlgebraicGeometry.AffineScheme
formalized as: Ideal.IsPrime.mul_notMem
formalized as: Ideal.primeCompl
formalized as: PrincipalIdealRing.isMaximal_of_irreducible
formalized as: Polynomial.irreducible_of_eisenstein_criterion
formalized as: Ideal.IsMaximal
formalized as: Ideal.IsMaximal.isPrime
formalized as: Ideal.IsPrime.isMaximal_of_ne_bot
formalized as: MvPolynomial.isMaximal_iff_eq_vanishingIdeal_singleton
formalized as: Ideal.Quotient.isDomain_iff_prime
formalized as: Ideal.isPrime_bot
formalized as: PrimeSpectrum.instIsEmpty
formalized as: Ideal.exists_maximal
formalized as: Ideal.isPrime_of_maximally_disjoint
formalized as: Ideal.IsPrime.comap
formalized as: Ideal.IsMinimalPrime
formalized as: minimalPrimes.equivIrreducibleComponents
formalized as: UniqueFactorizationMonoid.iff_exists_prime_mem_of_isPrime
formalized as: PrimeSpectrum.isIrreducible_iff_vanishingIdeal_isPrime
formalized as: AlgebraicGeometry.Scheme
formalized as: exists_le_isAssociatedPrime_of_isNoetherianRing
formalized as: Ideal.subset_union_prime
formalized as: Ideal.IsPrime.inf_le'
formalized as: Ideal.IsOka.isPrime_of_maximal_not
formalized as: Ideal.isOka_isPrincipal

Q207522
formalized as: MeasureTheory.pdf
formalized as: MeasureTheory.HasPDF
formalized as: MeasureTheory.withDensity_eq_iff_of_sigmaFinite
formalized as: MeasureTheory.pdf.IsUniform.pdf_eq
formalized as: ProbabilityTheory.gaussianPDFReal
formalized as: MeasureTheory.pdf.integral_mul_eq_integral
formalized as: MeasureTheory.noAtoms_withDensity
formalized as: MeasureTheory.pdf.indepFun_iff_pdf_prod_eq_pdf_mul_pdf
formalized as: MeasureTheory.pdf.integral_pdf_smul
formalized as: ProbabilityTheory.IndepFun.pdf_add_eq_lconvolution_pdf

Q7246880
formalized as: MeasureTheory.uniformOn_univ
formalized as: ProbabilityTheory.strong_law_ae

Q623472
formalized as: MeasureTheory.IsProbabilityMeasure
formalized as: MeasurableSpace
formalized as: MeasurableSet
formalized as: MeasureTheory.ProbabilityMeasure
formalized as: MeasureTheory.MeasureSpace
formalized as: MeasurableSet.iInter
formalized as: PMF
formalized as: MeasureTheory.Measure.IsComplete
formalized as: Measurable
formalized as: MeasureTheory.Measure.map
formalized as: MeasurableSpace.measurableSet_top
formalized as: MeasureTheory.borel
formalized as: ProbabilityTheory.cond
formalized as: ProbabilityTheory.cond_isProbabilityMeasure
formalized as: ProbabilityTheory.IndepSet
formalized as: ProbabilityTheory.IndepFun
formalized as: Disjoint
formalized as: MeasureTheory.measure_union
formalized as: Set.inter

Q5862903
formalized as: MeasurableSet
formalized as: IsProbabilityMeasure
formalized as: ProbabilityMeasure
formalized as: ProbabilityTheory.uniformOn
formalized as: PMF
formalized as: PMF.toMeasure_apply
formalized as: ProbabilityTheory.cdf
formalized as: ProbabilityTheory.monotone_cdf
formalized as: MeasureTheory.pdf
formalized as: ProbabilityTheory.cdf_measure_stieltjesFunction
formalized as: MeasureTheory.Measure
formalized as: MeasureTheory.Measure.rnDeriv
formalized as: MeasureTheory.TendstoInDistribution
formalized as: MeasureTheory.TendstoInMeasure
formalized as: MeasureTheory.TendstoInMeasure.tendstoInDistribution
formalized as: ProbabilityTheory.strong_law_ae
formalized as: ProbabilityTheory.tendstoInDistribution_inv_sqrt_mul_sum_sub

Q942423
formalized as: Module.Projective
formalized as: Module.Projective.of_free
formalized as: Module.projective_lifting_property
formalized as: Module.Projective.iff_split_of_projective
formalized as: Module.Projective.iff_split
formalized as: CategoryTheory.Projective.projective_iff_preservesEpimorphisms_preadditiveCoyoneda_obj
formalized as: Module.projective_def
formalized as: Module.Projective.of_split
formalized as: Module.Free.of_divisionRing
formalized as: Module.projective_of_isSemisimpleRing
formalized as: Module.Flat.of_projective
formalized as: Module.Flat.projective_of_finitePresentation
formalized as: CategoryTheory.ProjectiveResolution
formalized as: ModuleCat.enoughProjectives
formalized as: CategoryTheory.projectiveDimension
formalized as: CategoryTheory.projective_iff_hasProjectiveDimensionLT_one
formalized as: Module.projective_of_isLocalizedModule
formalized as: Module.freeLocus_eq_univ_iff
formalized as: Module.rankAtStalk
formalized as: Module.isLocallyConstant_rankAtStalk

Q877775
formalized as: Projectivization.equivSubmodule
formalized as: projectivizationSetoid
formalized as: Projectivization
formalized as: Projectivization.Subspace
formalized as: Projectivization.Subspace.instInfSet
formalized as: Projectivization.Subspace.span
formalized as: Projectivization.Independent
formalized as: Complex.exists_root
formalized as: AlgebraicGeometry.Proj
formalized as: littleWedderburn
formalized as: Projectivization.map
formalized as: Matrix.ProjGenLinGroup
formalized as: Module.Grassmannian

Q837863
formalized as: irrational_sqrt_two

Q15909572
formalized as: quadratic_eq_zero_iff
formalized as: discrim

Q472883
formalized as: legendreSym.quadratic_reciprocity
formalized as: legendreSym.quadratic_reciprocity_one_mod_four
formalized as: legendreSym.quadratic_reciprocity_three_mod_four
formalized as: ZMod.exists_sq_eq_neg_one_iff
formalized as: ZMod.exists_sq_eq_two_iff
formalized as: legendreSym.at_neg_one
formalized as: ZMod.pow_card_sub_one_eq_one
formalized as: legendreSym
formalized as: ZMod.exists_sq_eq_neg_two_iff
formalized as: jacobiSym.quadratic_reciprocity
formalized as: jacobiSym

Q918099
formalized as: Finite.exists_infinite_fiber

Q23937546
formalized as: Projectivization
formalized as: Projectivization.equivSubmodule
formalized as: projectivizationSetoid
formalized as: Matrix.op_smul_eq_vecMul
formalized as: Projectivization.generalLinearGroup_smul_def
formalized as: Matrix.ProjGenLinGroup
formalized as: OnePoint.smul_some_eq_ite

Q7322955
formalized as: TensorProduct.contractLeft
formalized as: Basis.ext_elem_iff
formalized as: MultilinearMap.alternatization
formalized as: fderiv_mul
formalized as: CovariantDerivative
formalized as: IsCovariantDerivativeOn.leibniz
formalized as: extDeriv
formalized as: VectorField.mlieBracket_self
formalized as: Matrix.one_apply
formalized as: CovariantDerivative.torsion

Q825857
formalized as: onePointEquivSphereOfFinrankEq
formalized as: OnePoint.equivProjectivization
formalized as: stereographic
formalized as: MeromorphicOn
formalized as: MDifferentiable.exists_eq_const_of_compactSpace

Q753035
formalized as: MDifferentiable.comp
formalized as: MDifferentiable.exists_eq_const_of_compactSpace

Q187235
formalized as: riemannZeta
formalized as: differentiableAt_riemannZeta
formalized as: riemannZeta_residue_one
formalized as: riemannZeta_eulerProduct_tprod
formalized as: Nat.exists_infinite_primes
formalized as: not_summable_one_div_on_primes
formalized as: riemannZeta_one_sub
formalized as: completedRiemannZeta_one_sub
formalized as: RiemannHypothesis
formalized as: riemannZeta_ne_zero_of_one_le_re
formalized as: riemannZeta_two_mul_nat
formalized as: riemannZeta_two
formalized as: riemannZeta_neg_nat_eq_bernoulli
formalized as: riemannZeta_neg_two_mul_nat_add_one
formalized as: riemannZeta_zero
formalized as: LSeries_zeta_mul_Lseries_moebius
formalized as: mellin
formalized as: hurwitzZeta

Q1208658
formalized as: CommRing
formalized as: IsDomain
formalized as: IsPrincipalIdealRing
formalized as: EuclideanDomain
formalized as: MvPolynomial.isMaximal_iff_eq_vanishingIdeal_singleton
formalized as: PrimeSpectrum
formalized as: Module
formalized as: Matrix.instRing
formalized as: IsSimpleRing.exists_ringEquiv_matrix_divisionRing
formalized as: jacobson_density
formalized as: IsSemiprimaryRing.isNoetherian_iff_isArtinian
formalized as: littleWedderburn
formalized as: ringKrullDim
formalized as: MvPolynomial.ringKrullDim_of_isNoetherianRing
formalized as: IsMoritaEquivalent
formalized as: CommRing.Pic
formalized as: Ring.jacobson
formalized as: Quaternion
formalized as: MvPolynomial.IsSymmetric
formalized as: MvPolynomial.esymmAlgEquiv

Q534131
formalized as: RootPairing.IsRootSystem
formalized as: RootPairing.IsCrystallographic
formalized as: RootPairing.IsReduced
formalized as: RootPairing.IsIrreducible
formalized as: RootPairing.Equiv
formalized as: RootPairing.rootSpan
formalized as: RootPairing.weylGroup
formalized as: LieAlgebra.IsKilling.rootSystem
formalized as: RootPairing.pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed
formalized as: RootPairing.Base
formalized as: RootPairing.Base.toWeightBasis
formalized as: RootPairing.coroot
formalized as: RootPairing.flip
formalized as: RootPairing.flip_flip
formalized as: RootPairing.Base.flip
formalized as: LieAlgebra.IsKilling.isSimple_iff_isIrreducible
formalized as: RootPairing.InvariantForm.exists_apply_eq_or

Q6500908
formalized as: IsSelfAdjoint
formalized as: LinearMap.IsSymmetric.eigenvectorBasis_apply_self_apply
formalized as: LinearPMap.graph
formalized as: LinearPMap.adjoint
formalized as: LinearMap.IsSymmetric
formalized as: LinearPMap.IsSelfAdjoint
formalized as: LinearMap.IsSymmetric.continuous
formalized as: ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric
formalized as: realPart_add_I_smul_imaginaryPart
formalized as: ContinuousLinearMap.IsPositive.isSelfAdjoint
formalized as: LinearMap.IsSymmetric.norm_eq_iSup_rayleighQuotient
formalized as: LinearMap.IsSymmetric.conj_eigenvalue_eq_self
formalized as: ContinuousLinearMap.eq_zero_of_forall_hasEigenvalue_eq_zero
formalized as: resolventSet
formalized as: spectrum
formalized as: IsSelfAdjoint.val_re_map_spectrum
formalized as: QuasispectrumRestricts.isSelfAdjoint
formalized as: LinearMap.IsSymmetric.eigenvectorBasis
formalized as: cfc
formalized as: MeasureTheory.Measure.MutuallySingular

Q12482
formalized as: Cardinal
formalized as: Cardinal.not_countable_real
formalized as: Cardinal.cantor
formalized as: Ordinal
formalized as: Set.Mem
formalized as: Set.Subset
formalized as: Set.ssubset_iff_subset_ne
formalized as: Set.union
formalized as: Set.inter
formalized as: Set.diff
formalized as: Set.compl
formalized as: symmDiff
formalized as: Set.prod
formalized as: Set.instEmptyCollectionSet
formalized as: Set.powerset
formalized as: ZFSet.rank

Q331350
formalized as: Affine.Simplex
formalized as: Affine.Simplex.mkOfPoint
formalized as: stdSimplex_fin_two
formalized as: Affine.Triangle
formalized as: stdSimplex
formalized as: Geometry.SimplicialComplex
formalized as: AbstractSimplicialComplex
formalized as: Affine.Simplex.face
formalized as: single_mem_stdSimplex
formalized as: AffineBasis.coord
formalized as: stdSimplex_unique
formalized as: Basis.addHaar_parallelepiped
formalized as: TopCat.toSSetObjEquiv
formalized as: CategoryTheory.SimplicialObject

Q420904
formalized as: LinearMap.singularValues
formalized as: LinearMap.card_support_singularValues
formalized as: LinearMap.IsSymmetric.hasEigenvalue_iSup_of_finiteDimensional
formalized as: Matrix.IsHermitian.spectral_theorem
formalized as: Matrix.frobenius_norm_def

Q190667
formalized as: Real.log_mul
formalized as: quadratic_eq_zero_iff
formalized as: Real.logb
formalized as: div_add_one

Q133327
formalized as: EuclideanSpace.dist_eq
formalized as: Isometry.dist_eq
formalized as: IsRiemannianManifold

Q3503315
formalized as: CategoryTheory.CohomologicalSpectralSequence
formalized as: CategoryTheory.SpectralSequence.page
formalized as: CategoryTheory.SpectralSequence
formalized as: CategoryTheory.SpectralSequence.Hom
formalized as: HomologicalComplex₂
formalized as: HomologicalComplex₂.total
formalized as: CategoryTheory.CohomologicalSpectralSequenceNat

Q1425077
formalized as: Matrix.IsHermitian.spectral_theorem
formalized as: LinearMap.IsSymmetric
formalized as: ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric
formalized as: LinearMap.IsSymmetric.conj_eigenvalue_eq_self
formalized as: Module.End.HasEigenvector
formalized as: LinearMap.IsSymmetric.direct_sum_isInternal
formalized as: Module.End.eigenspace
formalized as: LinearMap.IsSymmetric.eigenvectorBasis_apply_self_apply
formalized as: IsStarNormal
formalized as: ContinuousLinearMap.orthogonalComplement_iSup_eigenspaces_eq_bot
formalized as: cfc

Q2409122
formalized as: resolventSet
formalized as: spectrum
formalized as: resolvent
formalized as: Module.End.HasEigenvalue.mem_spectrum
formalized as: IsSelfAdjoint.mem_spectrum_eq_re
formalized as: InnerProductSpace.rankOne
formalized as: Module.End.HasEigenvalue
formalized as: OrthonormalBasis.sum_rankOne_eq_id
formalized as: OrthonormalBasis.sum_repr'
formalized as: IsSelfAdjoint.hasEigenvector_of_isMaxOn

Q203218
formalized as: Metric.sphere

Q164
formalized as: irrational_sqrt_two
formalized as: IsSquare
formalized as: DihedralGroup
formalized as: norm_add_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two

Q389813
formalized as: Real.sqrt
formalized as: irrational_sqrt_two
formalized as: irrational_sqrt_natCast_iff
formalized as: Real.cos_pi_div_four

Q193394
formalized as: EuclideanSpace.volume_ball_fin_two
formalized as: intermediate_value_Icc
formalized as: integral_inv
formalized as: irrational_pi

Q7598372
formalized as: MeasureTheory.Measure.map
formalized as: MeasurableSpace.CountablySeparated
formalized as: MeasurableSpace.CountablyGenerated
formalized as: MeasureTheory.Measure.condKernel

Q2500758
formalized as: IsLocalMin
formalized as: IsLocalMax
formalized as: IsLocalExtr
formalized as: IsExtrOn
formalized as: IsLocalExtr.deriv_eq_zero
formalized as: isLocalMin_of_deriv_deriv_pos

Q80918
formalized as: Nat.stirlingFirst
formalized as: Nat.stirlingSecond
formalized as: descPochhammer_zero
formalized as: Ring.descPochhammer_eq_factorial_smul_choose

Q484298
formalized as: chartAt
formalized as: ModelWithCorners.IsBoundaryPoint
formalized as: ModelWithCorners.IsInteriorPoint
formalized as: SmoothBumpCovering.exists_embedding_euclidean_of_compact

Q229102
formalized as: Function.Surjective
formalized as: Function.surjective_id
formalized as: Real.log_surjective
formalized as: Prod.fst_surjective
formalized as: Function.Bijective
formalized as: Function.RightInverse
formalized as: Function.surjective_iff_hasRightInverse
formalized as: Set.image_preimage_eq
formalized as: Function.injective_comp_right_iff_surjective
formalized as: CategoryTheory.Types.epi_iff_surjective
formalized as: CategoryTheory.IsSplitEpi.epi
formalized as: CategoryTheory.SplitEpi.section_
formalized as: CategoryTheory.IsSplitEpi
formalized as: Cardinal.mk_le_of_surjective
formalized as: Fintype.injective_iff_surjective_of_equiv
formalized as: Function.Surjective.comp
formalized as: Set.rangeFactorization_surjective
formalized as: Setoid.quotientKerEquivOfSurjective

Q849512
formalized as: Equiv.Perm
formalized as: Fintype.card_perm
formalized as: Equiv.Perm.subgroupOfMulAction
formalized as: Equiv.permUnique
formalized as: Equiv.Perm.permGroup
formalized as: Equiv.Perm.mul_apply
formalized as: Equiv.Perm.IsSwap
formalized as: Equiv.Perm.closure_isSwap
formalized as: Equiv.Perm.sign
formalized as: Equiv.Perm.sign_prod_list_swap
formalized as: Equiv.Perm.sign_mul
formalized as: alternatingGroup
formalized as: Equiv.Perm.alternatingGroup.index_eq_two
formalized as: Equiv.Perm.mclosure_swap_castSucc_succ
formalized as: Equiv.Perm.IsCycle
formalized as: Equiv.Perm.IsCycle.orderOf
formalized as: Equiv.Perm.card_support_eq_two
formalized as: Equiv.Perm.Disjoint
formalized as: Equiv.Perm.Disjoint.commute
formalized as: Equiv.Perm.truncCycleFactors
formalized as: Fin.revPerm
formalized as: Fin.rev_rev
formalized as: Equiv.Perm.isConj_iff_cycleType_eq
formalized as: Equiv.Perm.partition
formalized as: Equiv.Perm.fin_5_not_solvable
formalized as: Equiv.Perm.alternatingGroup.isSimpleGroup
formalized as: Subgroup
formalized as: Equiv.Perm.isCoatom_stabilizer
formalized as: Sylow.isPGroup'
formalized as: IteratedWreathProduct
formalized as: MulAction.IsPretransitive
formalized as: Polynomial.Gal.galAction_isPretransitive
formalized as: Subgroup.zpowers
formalized as: Equiv.Perm.lcm_cycleType
formalized as: MonoidAlgebra.instIsSemisimpleModule (Maschke)

Q21030012
formalized as: AffineIsometryEquiv.pointReflection

Q2431134
formalized as: Function.Even
formalized as: Function.Odd
formalized as: Matrix.IsSymm
formalized as: Matrix.IsSymm.apply
formalized as: Matrix.isSymm_diagonal
formalized as: Matrix.isHermitian_iff_isSymmetric
formalized as: Equiv.Perm
formalized as: Fintype.card_perm
formalized as: MvPolynomial.IsSymmetric
formalized as: MvPolynomial.esymmAlgHom_surjective
formalized as: SymmetricPower
formalized as: Polynomial.Gal.galActionHom
formalized as: CategoryTheory.Aut
formalized as: MulAut
formalized as: LinearMap.GeneralLinearGroup
formalized as: RingAut
formalized as: LinearMap.BilinForm.IsAlt.neg_eq
formalized as: Symmetric
formalized as: Isometry
formalized as: Congruent

Q11203
formalized as: Matrix.mulVec_eq_sum
formalized as: Matrix.mulVec
formalized as: Matrix.mulVec_cramer
formalized as: Matrix.inv_mulVec_eq_vec
formalized as: Matrix.mulVec_zero
formalized as: Matrix.mulVec_add
formalized as: Matrix.mulVecLin
formalized as: LinearMap.sub_mem_ker_iff
formalized as: LinearMap.mem_range

Q746550
formalized as: TangentBundle
formalized as: Bundle.TotalSpace.mk
formalized as: Bundle.TotalSpace.proj
formalized as: ContMDiff.contMDiff_tangentMap
formalized as: tangentBundleCore
formalized as: TangentSpace.vectorBundle
formalized as: ContMDiffSection

Q909601
formalized as: TangentSpace
formalized as: range_mfderiv_coe_sphere
formalized as: TangentBundle
formalized as: ContMDiff
formalized as: ContMDiffMap.algebra
formalized as: Derivation
formalized as: Derivation.map_algebraMap
formalized as: PointDerivation
formalized as: NormedSpace.fromTangentSpace
formalized as: lineDeriv
formalized as: tangentMap

Q1137206
formalized as: taylor_mean_remainder_lagrange
formalized as: hasDerivAt_iff_isLittleO
formalized as: taylorWithinEval
formalized as: taylor_isLittleO
formalized as: taylorWithin
formalized as: taylor_mean_remainder
formalized as: taylor_integral_remainder
formalized as: taylor_mean_remainder_bound
formalized as: exists_taylor_mean_remainder_bound
formalized as: AnalyticAt
formalized as: FormalMultilinearSeries.radius_inv_eq_limsup
formalized as: HasFPowerSeriesOnBall.tendstoUniformlyOn
formalized as: expNegInvGlue.not_analyticAt_zero
formalized as: DifferentiableOn.analyticOnNhd
formalized as: Complex.circleIntegral_div_sub_of_differentiable_on_off_countable
formalized as: DifferentiableOn.contDiffOn
formalized as: Complex.norm_iteratedDeriv_le_of_forall_mem_sphere_norm_le
formalized as: HasFDerivAt
formalized as: fderiv

Q214856
formalized as: DiscreteTiling.Prototile

Q65943
formalized as: EuclideanGeometry.angle_add_angle_add_angle_eq_pi
formalized as: FermatLastTheorem
formalized as: even_iff_two_dvd
formalized as: FirstOrder.Language.Theory
formalized as: FirstOrder.Language.Sentence

Q1154787
formalized as: jacobiTheta₂
formalized as: jacobiTheta₂_add_left'
formalized as: jacobiTheta₂_add_left
formalized as: jacobiTheta_S_smul
formalized as: jacobiTheta₂_functional_equation
formalized as: Complex.betaIntegral
formalized as: Complex.betaIntegral_eq_Gamma_mul_div
formalized as: Nat.Partition
formalized as: Nat.Partition.hasProd_powerSeriesMk_card_restricted
formalized as: pentagonal
formalized as: Nat.Partition.distincts
formalized as: Nat.Partition.hasProd_powerSeriesMk_card_countRestricted

Q2393193
formalized as: Turing.TM2ComputableInPolyTime

Q737279
formalized as: irrational_sqrt_two
formalized as: Nat.exists_infinite_primes
formalized as: ZMod.chineseRemainder
formalized as: Real.sin
formalized as: sq_add_sq_mul_sq_add_sq
formalized as: EuclideanSpace.volume_ball
formalized as: Real.arctan
formalized as: add_pow
formalized as: fermatLastTheoremThree
formalized as: EuclideanGeometry.law_sin
formalized as: Nat.rec
formalized as: Real.sin_add
formalized as: pow_eq_pow_iff_of_ne_zero
formalized as: exists_deriv_eq_zero
formalized as: Complex.hasSum_arctan
formalized as: exists_deriv_eq_slope
formalized as: intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le
formalized as: Real.hasSum_pow_div_log_of_abs_lt_1
formalized as: taylor_mean_remainder_lagrange
formalized as: deriv.lhopital_zero_nhds
formalized as: bernoulli
formalized as: taylorWithin
formalized as: Complex.cos_add_sin_mul_I_pow
formalized as: ProbabilityTheory.gaussianReal
formalized as: hasSum_zeta_two
formalized as: ProbabilityTheory.cond_eq_inv_mul_cond_mul
formalized as: irrational_pi
formalized as: MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable
formalized as: Complex.exists_root
formalized as: intermediate_value_Icc
formalized as: Metric.tendsto_nhds_nhds
formalized as: Complex.circleIntegral_sub_inv_smul_of_differentiable_on_off_countable
formalized as: Nat.infinite_setOf_prime_and_eq_mod
formalized as: TendstoUniformly
formalized as: Quaternion
formalized as: BooleanAlgebra
formalized as: IsRiemannianManifold
formalized as: RiemannHypothesis
formalized as: Cardinal.not_countable_real
formalized as: CommRing
formalized as: MeasureTheory.IsProbabilityMeasure
formalized as: Computable

Q42989
formalized as: TopologicalSpace
formalized as: Homeomorph
formalized as: ContinuousMap.HomotopyEquiv
formalized as: IsOpen
formalized as: IsClosed
formalized as: IsClopen
formalized as: TopologicalSpace.OpenNhds
formalized as: Continuous
formalized as: ChartedSpace
formalized as: IsCompact
formalized as: IsConnected
formalized as: MetricSpace
formalized as: Metric.isOpen_iff
formalized as: subgroupIsFreeOfIsFree
formalized as: CategoryTheory.GrothendieckTopology

Q173091
formalized as: Transcendental
formalized as: Transcendental.irrational
formalized as: transcendental_liouvilleNumber
formalized as: Liouville
formalized as: Liouville.transcendental
formalized as: Algebraic.countable

Q208216
formalized as: dist_triangle
formalized as: norm_add_le
formalized as: EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two
formalized as: dist_le_range_sum_dist
formalized as: sameRay_iff_norm_add
formalized as: Real.norm_eq_abs
formalized as: PiLp.norm_eq_sum
formalized as: EuclideanSpace.norm_eq
formalized as: norm_inner_eq_norm_iff
formalized as: Real.Lp_add_le
formalized as: Filter.Tendsto.cauchySeq
formalized as: abs_norm_sub_norm_le
formalized as: lipschitzWith_one_norm

Q8084
formalized as: Real.sin
formalized as: Real.cos
formalized as: Real.tan
formalized as: Real.cos_pi_div_two_sub
formalized as: Circle
formalized as: Real.arctan
formalized as: Complex.hasSum_sin
formalized as: Complex.exp_mul_I
formalized as: EuclideanGeometry.sin_angle_mul_dist_eq_sin_angle_mul_dist
formalized as: EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_sub_two_mul_dist_mul_dist_mul_cos_angle
formalized as: Real.sin_sq_add_cos_sq
formalized as: Complex.sin

Q163310
formalized as: Turing.TM0.Machine
formalized as: ComputablePred.halting_problem
formalized as: Turing.TM0.Cfg

Q658429
formalized as: VectorBundle
formalized as: Bundle.Trivial.vectorBundle
formalized as: tangentBundleCore
formalized as: FiberBundle
formalized as: Bundle.Trivialization
formalized as: Bundle.Trivial
formalized as: VectorBundleCore.coordChange
formalized as: FiberBundleCore.coordChange_comp
formalized as: FiberBundleCore.fiberBundle
formalized as: VectorBundle.prod
formalized as: Bundle.ContinuousLinearMap.vectorBundle
formalized as: VectorBundle.pullback
formalized as: RiemannianBundle
formalized as: ContMDiffVectorBundle

Q200802
formalized as: crossProduct
formalized as: triple_product_eq_det
formalized as: MeasureTheory.integral_divergence_prod_Icc_of_hasFDerivAt_off_countable_of_le
formalized as: HasFDerivAt
formalized as: IsLocalExtr.fderiv_eq_zero
formalized as: EuclideanSpace
formalized as: TangentBundle

Q1970172
formalized as: VonNeumannAlgebra
formalized as: WStarAlgebra
formalized as: IsStarProjection

Q37172
formalized as: fourierIntegral_gaussian

Q831390
formalized as: MeasureTheory.Lp

Q659746
formalized as: IsWellOrder
formalized as: WellOrder
formalized as: WellFounded.has_min
formalized as: SuccOrder.ofLinearWellFoundedLT
formalized as: WellFoundedLT.conditionallyCompleteLinearOrderBot
formalized as: isWellOrder_lt
formalized as: Ordinal.type
formalized as: exists_wellFoundedLT
formalized as: WellFoundedLT.induction
formalized as: type_nat_lt
formalized as: PrincipalSeg.ofElement
formalized as: InitialSeg.isLowerSet_range
formalized as: ZFSet.IsOrdinal
formalized as: PrincipalSeg.irrefl
formalized as: InitialSeg.total
formalized as: InitialSeg.image_Iio
formalized as: Ordinal
formalized as: Preorder.topology
formalized as: IsCofinal
formalized as: Ordinal.type_fintype

Q576728
formalized as: FundamentalGroup

Q3573180
formalized as: Real.hasSum_arctan
formalized as: Real.tendsto_sum_pi_div_four
formalized as: Real.pi_lt_d20
formalized as: Real.hasSum_sin
formalized as: Real.cos_add
formalized as: taylor_mean_remainder_lagrange

Q290810
formalized as: zorn_le
formalized as: IsChain.exists_maxChain
formalized as: PartialOrder
formalized as: GE.ge
formalized as: LinearOrder
formalized as: Subtype.partialOrder
formalized as: IsChain
formalized as: IsMax
formalized as: upperBounds
formalized as: exists_maximal_of_chains_bounded
formalized as: zorn_le_nonempty_Ici₀
formalized as: Module.Basis.exists_basis
formalized as: Ideal.exists_maximal
formalized as: isCompact_univ_pi
formalized as: ChainCompletePartialOrder.nonempty_fixedPoints_of_inflationary
formalized as: exists_extension_of_le_sublinear
formalized as: Ultrafilter.exists_le