| Name | Category | Theorems |
|---|
Irreducible 📖 | CompData | 163 mathmath: Prime.irreducible, ZMod.irreducible_of_dvd_cyclotomic_of_natDegree, Associates.isAtom_iff, FixedPoints.minpoly.irreducible, Polynomial.cyclotomic.irreducible, Polynomial.irreducible_of_mirror, Associates.factors_mul, Associates.prod_top, X_pow_sub_C_irreducible_iff_of_odd, Polynomial.irreducible_of_monic, X_pow_sub_C_irreducible_of_odd, Polynomial.irreducible_iff_roots_eq_zero_of_degree_le_three, Polynomial.irreducible_comp, RatFunc.irreducible_min_polynomial_valuation_lt_one_and_ne_zero, MvPolynomial.irreducible_mul_X_add, Associates.irreducible_mk, not_irreducible_pow, Polynomial.IsUnitTrinomial.irreducible_of_coprime, irreducible_mul_units, PadicInt.irreducible_p, Polynomial.exists_monic_irreducible_factor, X_pow_sub_C_irreducible_iff_forall_prime_of_odd, WeierstrassCurve.Affine.irreducible_polynomial, Polynomial.IsUnitTrinomial.irreducible_of_isCoprime, Associates.pow_factors, Polynomial.irreducible_of_eisenstein_criterion, IsSquare.not_irreducible, Polynomial.irreducible_mul_leadingCoeff_inv, IsDiscreteValuationRing.irreducible_of_span_eq_maximalIdeal, Polynomial.separable_or, UniqueFactorizationMonoid.irreducible_iff_prime, Polynomial.Monic.irreducible_iff_lt_natDegree_lt, Associates.count_some, Associates.count_zero, irreducible_subset_of_submonoidClosure_eq_top, Polynomial.IsPrimitive.irreducible_of_irreducible_map_of_injective, IsDedekindDomain.HeightOneSpectrum.irreducible, Associates.factors_zero, Nat.irreducible_iff_prime, Polynomial.IsPrimitive.irreducible_iff_irreducible_map_fraction_map, MvPolynomial.irreducible_of_forall_totalDegree_le, irreducible_or_factor, Associates.factors_subsingleton, Associated.irreducible, X_pow_sub_C_irreducible_iff_of_prime_pow, Associates.mem_factorSet_some, Associates.factors_mk, Polynomial.X_pow_sub_X_sub_one_irreducible, MvPolynomial.irreducible_of_disjoint_support, IsDiscreteValuationRing.exists_irreducible, Polynomial.generalizedEisenstein, Polynomial.Separable.map_irreducible_of_isPurelyInseparable, Polynomial.fact_irreducible_factor, IsDiscreteValuationRing.irreducible_iff_uniformizer, Irreducible.exists_dvd_monic_irreducible_of_isIntegral, Polynomial.Monic.irreducible_of_irreducible_map, WfDvdMonoid.not_unit_iff_exists_factors_eq, Associates.prod_add, Associates.factors_le, MvPolynomial.irreducible_sumSMulX, Polynomial.IsPrimitive.Int.irreducible_iff_irreducible_map_cast, PowerSeries.X_irreducible, Associates.factors_prime_pow, Irreducible.map, WfDvdMonoid.exists_irreducible_factor, isMulIndecomposable_id_univ, Associates.factors_mono, Associates.factors_eq_some_iff_ne_zero, Associates.map_subtype_coe_factors', WittVector.irreducible, Associates.mem_factors'_iff_dvd, Polynomial.of_irreducible_expand_pow, UniqueFactorizationMonoid.irreducible_of_factor, Polynomial.cyclotomic_irreducible_of_irreducible_pow, X_pow_sub_C_irreducible_of_prime, X_pow_mul_sub_C_irreducible, Polynomial.irreducible_of_degree_eq_one_of_isRelPrime_coeff, irreducible_iff_prime_of_exists_prime_factors, RatFunc.irreducible_minpolyX, Polynomial.Monic.irreducible_iff_natDegree, Polynomial.Monic.irreducible_of_irreducible_map_of_isPrime_nilradical, RatFunc.irreducible_minpolyX', MvPolynomial.of_irreducible_expand, Associates.mem_factorSet_top, KummerDedekind.Ideal.irreducible_map_of_irreducible_minpoly, Polynomial.IsUnitTrinomial.irreducible_of_coprime', Polynomial.irreducible_of_degree_le_three_of_not_isRoot, Irreducible.of_map, isSplittingField_AdjoinRoot_X_pow_sub_C, Associates.factors_eq_top_iff_zero, irreducible_iff_prime_of_existsUnique_irreducible_factors, Cardinal.not_irreducible_of_aleph0_le, MulEquiv.irreducible_iff, Polynomial.Monic.irreducible_iff_degree_lt, not_irreducible_expand, PrincipalIdealRing.factors_spec, Polynomial.irreducible_factor, Ideal.irreducible_of_irreducible_absNorm, irreducible_units_mul, not_irreducible_zero, Associates.irreducible_of_mem_factorSet, finite_irreducible, not_irreducible_of_not_unit_dvdNotUnit, irreducible_sq_not_dvd_iff_eq_zero_and_no_irreducibles_or_squarefree, Polynomial.irreducible_iff_degree_lt, Polynomial.X_pow_sub_X_sub_one_irreducible_rat, DivisorChain.second_of_chain_is_irreducible, Polynomial.mem_normalizedFactors_iff, MvPolynomial.irreducible_toPolynomialAdjoinImageCompl, not_irreducible_one, Associates.irreducible_iff_prime_iff, Polynomial.cyclotomic.irreducible_rat, Submonoid.FG.finite_irreducible_mem_submonoidClosure, X_pow_sub_C_irreducible_of_prime_pow, irreducible_iff, Associates.FactorSet.coe_add, UniqueFactorizationMonoid.mem_normalizedFactors_iff', Polynomial.isIntegrallyClosed_iff', UniqueFactorizationMonoid.irreducible_of_normalized_factor, Polynomial.exists_irreducible_of_natDegree_ne_zero, Polynomial.irreducible_X, Polynomial.Monic.not_irreducible_iff_exists_add_mul_eq_coeff, Polynomial.Monic.irreducible_iff_natDegree', Associates.prime_pow_le_iff_le_bcount, MvPolynomial.irreducible_of_totalDegree_eq_one, irreducible_mem_submonoidClosure_subset, Polynomial.exists_irreducible_of_natDegree_pos, irreducible_mul_iff, MvPolynomial.irreducible_sumSMulXSMulY, Nat.irreducible_iff_nat_prime, Polynomial.not_irreducible_C, irreducible_iff_prime, Polynomial.Monic.irreducible_iff_irreducible_map_fraction_map, WfDvdMonoid.exists_factors, associates_irreducible_iff_prime, minpoly.irreducible, Polynomial.IsEisensteinAt.irreducible, Polynomial.irreducible_X_sub_C, Submonoid.closure_irreducible, Polynomial.irreducible_C_mul_X_add_C, Associates.factors_self, Associates.prod_le, Polynomial.cyclotomic_irreducible_pow_of_irreducible_pow, Polynomial.Monic.irreducible_of_degree_eq_one, Associated.irreducible_iff, Associates.factors_one, IsDedekindDomain.HeightOneSpectrum.associates_irreducible, Polynomial.irreducible_iff_lt_natDegree_lt, Associates.FactorSet.sup_add_inf_eq_add, ConjRootClass.irreducible_minpoly, Associates.mem_factors'_of_dvd, Polynomial.irreducible_of_degree_eq_one, irreducible_isUnit_mul, Associates.prod_coe, irreducible_X_pow_sub_C_of_root_adjoin_eq_top, Polynomial.Monic.irreducible_iff_roots_eq_zero_of_degree_le_three, Associates.FactorSet.prod_eq_zero_iff, X_pow_sub_C_irreducible_iff_of_prime, Polynomial.irreducible_of_dvd_cyclotomic_of_natDegree, Polynomial.exists_irreducible_of_degree_pos, isCyclic_tfae, irreducible_mul_isUnit, Polynomial.of_irreducible_expand
|
IrreducibleSpace 📖 | CompData | 22 mathmath: AlgebraicGeometry.irreducibleSpace_of_isIntegral, AlgebraicGeometry.Scheme.instIrreducibleSpaceCarrierCarrierCommRingCatIrreducibleComponent, AlgebraicGeometry.GeometricallyIrreducible.geometrically_irreducibleSpace, Function.Surjective.irreducibleSpace, AlgebraicGeometry.instIsClosedUnderIsomorphismsSchemeIrreducibleSpaceCarrierCarrierCommRingCat, PrimeSpectrum.irreducibleSpace_iff_isPrime_nilradical, isIrreducible_iff_irreducibleSpace, AlgebraicGeometry.instIrreducibleSpaceCarrierCarrierCommRingCatSpecOfIsDomainCarrier, AlgebraicGeometry.instIrreducibleSpaceCarrierCarrierCommRingCatPullbackSchemeOfGeometricallyIrreducibleOfUniversallyOpen, Subtype.irreducibleSpace, Homeomorph.irreducibleSpace_iff, AlgebraicGeometry.isIntegral_iff_irreducibleSpace_and_isReduced, AlgebraicGeometry.GeometricallyIrreducible.irreducibleSpace_of_subsingleton, AlgebraicGeometry.instIrreducibleSpaceCarrierCarrierCommRingCatFiberOfGeometricallyIrreducible, AlgebraicGeometry.GeometricallyIrreducible.eq_geometrically, AlgebraicGeometry.geometricallyIrreducible_iff, instIrreducibleSpaceCofiniteTopologyOfInfinite, AlgebraicGeometry.instIrreducibleSpaceCarrierCarrierCommRingCatPullbackSchemeOfGeometricallyIrreducibleOfUniversallyOpen_1, PrimeSpectrum.irreducibleSpace, AlgebraicGeometry.GeometricallyIrreducible.irreducibleSpace, irreducibleSpace_def, Topology.IsOpenEmbedding.irreducibleSpace
|
IsIrreducible 📖 | MathDef | 34 mathmath: PrimeSpectrum.vanishingIdeal_isClosed_isIrreducible, isIrreducible_iff_sUnion_isClosed, isIrreducible_iff_singleton, TopologicalSpace.NoetherianSpace.exists_finset_irreducible, TopologicalSpace.NoetherianSpace.exists_finite_set_isClosed_irreducible, PrimeSpectrum.isIrreducible_zeroLocus_iff_of_radical, isIrreducible_iff_sInter, isIrreducible_iff_irreducibleSpace, IsGenericPoint.isIrreducible, TopologicalSpace.IrreducibleCloseds.instCanLiftSetCoeAndIsIrreducibleIsClosed, PrimeSpectrum.isIrreducible_zeroLocus_iff, TopologicalSpace.IrreducibleCloseds.is_irreducible', PrimeSpectrum.vanishingIdeal_isIrreducible, IrreducibleSpace.isIrreducible_univ, TopologicalSpace.IrreducibleCloseds.isIrreducible, IsPreirreducible.subset_irreducible, isIrreducible_singleton, IsIrreducible.image, TopologicalSpace.IrreducibleCloseds.isIrreducible', IsIrreducible.closure, TopologicalSpace.IrreducibleCloseds.equivSubtype_apply, IsIrreducible.of_subtype, TopologicalSpace.NoetherianSpace.exists_finite_set_closeds_irreducible, IsIrreducible.preimage_of_isPreirreducible_fiber, TopologicalSpace.IrreducibleCloseds.equivSubtype'_apply, IsIrreducible.preimage, TopologicalSpace.IrreducibleCloseds.equivSubtype_symm_apply, PrimeSpectrum.isIrreducible_iff_vanishingIdeal_isPrime, isIrreducible_irreducibleComponent, irreducibleComponents_eq_maximals_closed, AlgebraicGeometry.Scheme.Hom.isIrreducible_preimage, isIrreducible_iff_closure, irreducibleSpace_def, TopologicalSpace.IrreducibleCloseds.equivSubtype'_symm_apply
|
IsPreirreducible 📖 | MathDef | 21 mathmath: IsPreirreducible.of_subtype, isPreirreducible_empty, IsPreirreducible.image, isPreirreducible_iff_preirreducibleSpace, IsPreirreducible.open_subset, isPreirreducible_iff_isClosed_union_isClosed, PreirreducibleSpace.isPreirreducible_univ, IsPreirreducible.interior, IsPreirreducible.preimage_of_dense_isPreirreducible_fiber, isPreirreducible_iff_closure, isPreirreducible_singleton, IsIrreducible.isPreirreducible, isPreirreducible_iff_forall_mem_subset_closure_singleton, IsPreirreducible.of_subset_iUnion, IsPreirreducible.closure, irreducibleComponent_property, Set.Subsingleton.isPreirreducible, exists_preirreducible, IsPreirreducible.preimage_of_isPreirreducible_fiber, IsPreirreducible.preimage, isPreirreducible_iff_subsingleton
|
PreirreducibleSpace 📖 | CompData | 8 mathmath: isPreirreducible_iff_preirreducibleSpace, Function.Surjective.preirreducibleSpace, PreirreducibleSpace.of_isOpenCover, instPreirreducibleSpaceOfSubsingleton, Subtype.preirreducibleSpace, PreirreducibleSpace.of_forall_nonempty_inter, Topology.IsOpenEmbedding.preirreducibleSpace, IrreducibleSpace.toPreirreducibleSpace
|
irreducibleComponent 📖 | CompOp | 7 mathmath: irreducibleComponent_mem_irreducibleComponents, eq_irreducibleComponent, mem_irreducibleComponent, isIrreducible_irreducibleComponent, irreducibleComponent_subset_connectedComponent, isClosed_irreducibleComponent, irreducibleComponent_property
|
irreducibleComponents 📖 | CompOp | 23 mathmath: irreducibleComponent_mem_irreducibleComponents, genericPoints.component_injective, genericPoints.equiv_symm_apply, irreducibleComponents_eq_singleton, PrimeSpectrum.vanishingIdeal_irreducibleComponents, AlgebraicGeometry.Scheme.Hom.irreducibleComponentsEquiv_symm_apply_coe, genericPoints.isGenericPoint_ofComponent, PrimeSpectrum.zeroLocus_minimalPrimes, genericPoints.component_surjective, sUnion_irreducibleComponents, genericPoints.equiv_apply, PrimeSpectrum.zeroLocus_ideal_mem_irreducibleComponents, genericPoints.isGenericPoint, preimage_mem_irreducibleComponents, preimage_mem_irreducibleComponents_of_isPreirreducible_fiber, closure_sUnion_irreducibleComponents_diff_singleton, AlgebraicGeometry.Scheme.Hom.irreducibleComponentsEquiv_apply_coe, image_mem_irreducibleComponents_of_isPreirreducible_fiber, TopologicalSpace.NoetherianSpace.finite_irreducibleComponents, irreducibleComponents_eq_maximals_closed, exists_mem_irreducibleComponents_subset_of_isIrreducible, AlgebraicGeometry.finite_irreducibleComponents_of_isNoetherian, PrimeSpectrum.vanishingIdeal_mem_minimalPrimes
|
irreducibleComponentsEquivOfIsPreirreducibleFiber 📖 | CompOp | — |