Documentation Verification Report

Maximal

📁 Source: Mathlib/RingTheory/Ideal/Maximal.lean

Statistics

Metric	Count
Definitions `IsMaximal`, `Maximal`, `Maximal`	3
Theorems `coprime_of_ne`, `eq_of_le`, `exists_inv`, `isPrime`, `isPrime'`, `lt_top`, `ne_top`, `out`, `bot_isMaximal`, `exists_disjoint_powers_of_span_eq_top`, `exists_le_maximal`, `exists_le_prime_disjoint`, `exists_le_prime_notMem_of_isIdempotentElem`, `exists_maximal`, `instIsCoatomic`, `instNontrivial`, `isMaximal_def`, `isMaximal_iff`, `isPrime_iff_of_isPrincipalIdealRing`, `isPrime_iff_of_isPrincipalIdealRing_of_noZeroDivisors`, `isPrime_of_maximally_disjoint`, `maximal_of_no_maximal`, `ne_top_iff_exists_maximal`, `sInf_isPrime_of_isChain`, `span_singleton_lt_span_singleton`, `span_singleton_prime`	26
Total	29

Ideal

Definitions

Name	Category	Theorems
`IsMaximal` 📖	CompData	107 math math: `eq_jacobson_iff_sInf_maximal`, `IsMaximal.map_bijective`, `exists_maximal`, `isMaximal_of_isIntegral_of_isMaximal_comap'`, `isMaximal_of_mem_primesOver`, `PrimeSpectrum.discreteTopology_iff_finite_isMaximal_and_sInf_le_nilradical`, `IsDedekindDomain.HeightOneSpectrum.isMaximal`, `jacobson.isMaximal`, `IsMaximal.of_liesOver_isMaximal`, `AlgebraicClosure.maxIdeal.isMaximal`, `map_eq_top_or_isMaximal_of_surjective`, `comap_isMaximal_of_equiv`, `IsIntegralClosure.isMaximal_of_isMaximal_comap`, `IsLocalRing.maximal_ideal_unique`, `exists_maximal_ideal_liesOver_of_isIntegral`, `jacobson_bot_polynomial_le_sInf_map_maximal`, `IsPrime.isMaximal`, `isMaximal_of_isPrime`, `RingHom.ker_isMaximal_of_surjective`, `Ring.krullDimLE_zero_and_isLocalRing_tfae`, `Ring.HasFiniteQuotients.maximalOfPrime`, `Algebra.ker_algebraMap_isMaximal_of_isIntegral`, `MaximalSpectrum.isMaximal`, `PrimeSpectrum.isMax_iff`, `IsLocalization.isMaximal_iff_isMaximal_disjoint`, `isJacobsonRing_iff_sInf_maximal`, `AlgebraicGeometry.IsAffineOpen.primeIdealOf_isMaximal_of_isClosed`, `Ring.krullDimLE_one_iff_of_noZeroDivisors`, `IsMaximal.map_of_surjective_of_ker_le`, `DualNumber.isMaximal_span_singleton_eps`, `IsMaximal.comap_bijective`, `Ring.krullDimLE_zero_iff`, `isMaximal_iff_of_bijective`, `Int.ideal_span_isMaximal_of_prime`, `exists_isMaximal_height`, `Ring.krullDimLE_one_iff`, `sup_primeHeight_of_maximal_eq_ringKrullDim`, `IsMaximal.comap_piEvalRingHom`, `ContinuousMap.ideal_isMaximal_iff`, `comap_isMaximal_of_surjective`, `AdjoinRoot.span_maximal_of_irreducible`, `exists_ideal_liesOver_maximal_of_isIntegral`, `MaximalSpectrum.range_asIdeal`, `MaximalSpectrum.equivSubtype_symm_apply_asIdeal`, `PrimeSpectrum.isClosed_singleton_iff_isMaximal`, `exists_max_ideal_of_mem_nonunits`, `IsPrime.to_maximal_ideal`, `isMaximal_of_primeHeight_eq_ringKrullDim`, `isMaximal_iff`, `IsMaximal.of_isLocalization_of_disjoint`, `Polynomial.isMaximal_comap_C_of_isJacobsonRing`, `IntegralClosure.isMaximal_of_isMaximal_comap`, `MaximalSpectrum.equivSubtype_apply_coe`, `eq_jacobson_iff_notMem`, `Polynomial.isMaximal_comap_C_of_isMaximal`, `isSimpleModule_iff_quot_maximal`, `IsLocalization.AtPrime.isMaximal_map`, `IsLocalRing.maximalIdeal.isMaximal`, `IsMaximal.of_isMaximal_liesOver`, `IsLocalRing.not_isLocalRing_tfae`, `IsArtinianRing.isMaximal_of_isPrime`, `PrimeSpectrum.stableUnderSpecialization_singleton`, `PrincipalIdealRing.isMaximal_of_irreducible`, `Ring.KrullDimLE.minimalPrimes_eq_setOf_isMaximal`, `bot_isMaximal`, `isMaximal_comap_of_isIntegral_of_isMaximal`, `Ring.DimensionLEOne.maximalOfPrime`, `WeakDual.ker_isMaximal`, `ne_top_iff_exists_maximal`, `IsLocalRing.isMaximal_iff`, `map_isMaximal_of_equiv`, `isMaximal_comap_iff_of_bijective`, `Module.exists_ltSeries_support_isMaximal_last_of_ltSeries_support`, `Quotient.maximal_of_isField`, `IsLocalization.isMaximal_of_isMaximal_disjoint`, `exists_ideal_over_maximal_of_isIntegral`, `exists_le_maximal`, `isMaximal_map_iff_of_bijective`, `PrimeSpectrum.exists_maximal_notMem_range_sigmaToPi_of_infinite`, `IsArtinianRing.isPrime_iff_isMaximal`, `PrimeSpectrum.isMaximal_of_toPiLocalization_surjective`, `primesOver.isMaximal`, `Ring.isField_iff_maximal_bot`, `IsSimpleModule.annihilator_isMaximal`, `ContinuousMap.idealOf_compl_singleton_isMaximal`, `IsPrime.isMaximal'`, `isLocal_iff`, `MvPolynomial.instIsMaximalVanishingIdealSingletonForallSet`, `Ring.exists_maximal_of_not_isField`, `bot_quotient_isMaximal_iff`, `MixedCharZero.reduce_to_maximal_ideal`, `isMaximal_iff_isPrime`, `isMaximal_comap_of_isIntegral_of_isMaximal'`, `Ring.jacobson_eq_sInf_isMaximal`, `IsMaximal.under`, `MvPolynomial.isMaximal_iff_eq_vanishingIdeal_singleton`, `NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply`, `ContinuousMap.idealOfSet_isMaximal_iff`, `instIsMaximalOfIsPrimeOfKrullDimLEOfNatNat`, `Quotient.maximal_ideal_iff_isField_quotient`, `IsLocal.out`, `IsSimpleModule.ker_toSpanSingleton_isMaximal`, `Ring.krullDimLE_one_iff_of_isPrime_bot`, `comap_jacobson`, `isMaximal_of_isIntegral_of_isMaximal_comap`, `IsArtinianRing.setOf_isMaximal_finite`, `isMaximal_def`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bot_isMaximal` 📖	mathematical	—	`IsMaximal` `DivisionSemiring.toSemiring` `Bot.bot` `Ideal` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`eq_top_iff_one` `NeZero.one` `GroupWithZero.toNontrivial` `eq_bot_or_top` `ne_of_gt`
`exists_disjoint_powers_of_span_eq_top` 📖	mathematical	`span` `CommSemiring.toSemiring` `Top.top` `Ideal` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`Set` `Set.instMembership` `Disjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `SetLike.coe` `Ideal` `CommSemiring.toSemiring` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Submonoid.instSetLike` `Submonoid.powers`	—	`exists_le_maximal` `IsMaximal.out` `Set.not_subset` `span_le` `eq_top_iff` `Set.disjoint_left` `IsPrime.mem_of_pow_mem` `IsMaximal.isPrime`
`exists_le_maximal` 📖	mathematical	—	`Ideal` `IsMaximal` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`IsCoatomic.eq_top_or_exists_le_coatom` `instIsCoatomic`
`exists_le_prime_disjoint` 📖	mathematical	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `SetLike.coe` `Ideal` `CommSemiring.toSemiring` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Submonoid.instSetLike`	`Ideal` `CommSemiring.toSemiring` `IsPrime` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `SetLike.coe` `Submodule.setLike` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Submonoid.instSetLike`	—	`zorn_le_nonempty₀` `isEmpty_or_nonempty` `Set.disjoint_left` `Submodule.mem_iSup_of_directed` `IsChain.directed` `instReflLe` `sSup_eq_iSup'` `le_sSup` `isPrime_of_maximally_disjoint` `Maximal.not_prop_of_gt`
`exists_le_prime_notMem_of_isIdempotentElem` 📖	mathematical	`IsIdempotentElem` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Semiring.toModule`	`Ideal` `CommSemiring.toSemiring` `IsPrime` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike`	—	`Set.disjoint_right` `IsIdempotentElem.coe_powers` `ne_top_iff_one` `Submodule.mem_top` `exists_le_prime_disjoint` `Submonoid.mem_powers`
`exists_maximal` 📖	mathematical	—	`Ideal` `IsMaximal`	—	`exists_le_maximal` `bot_ne_top` `Submodule.instNontrivial`
`instIsCoatomic` 📖	mathematical	—	`IsCoatomic` `Ideal` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.instOrderTop`	—	`CompleteLattice.coatomic_of_top_compact` `isCompactElement_top`
`instNontrivial` 📖	mathematical	—	`Nontrivial` `Ideal`	—	`exists_maximal` `nontrivial_of_ne`
`isMaximal_def` 📖	mathematical	—	`IsMaximal` `IsCoatom` `Ideal` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.instOrderTop`	—	`IsMaximal.out`
`isMaximal_iff` 📖	mathematical	—	`IsMaximal` `Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`instIsConcreteLE`
`isPrime_iff_of_isPrincipalIdealRing` 📖	mathematical	—	`IsPrime` `CommSemiring.toSemiring` `Prime` `CommSemiring.toCommMonoidWithZero` `span` `Set` `Set.instSingletonSet`	—	`Submodule.IsPrincipal.principal` `IsPrincipalIdealRing.principal` `span_singleton_prime` `span_singleton_zero` `Prime.ne_zero`
`isPrime_iff_of_isPrincipalIdealRing_of_noZeroDivisors` 📖	mathematical	—	`IsPrime` `CommSemiring.toSemiring` `Bot.bot` `Ideal` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Prime` `CommSemiring.toCommMonoidWithZero` `span` `Set` `Set.instSingletonSet`	—	`isPrime_iff_of_isPrincipalIdealRing` `isPrime_bot`
`isPrime_of_maximally_disjoint` 📖	mathematical	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `SetLike.coe` `Ideal` `CommSemiring.toSemiring` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Submonoid.instSetLike`	`IsPrime` `CommSemiring.toSemiring`	—	`Submonoid.one_mem` `Submodule.lt_sup_iff_notMem` `Disjoint.ne_of_mem` `add_mem` `mul_mem_left` `mul_mem_right` `instIsTwoSided` `Submonoid.mul_mem` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_gt`
`maximal_of_no_maximal` 📖	mathematical	`IsMaximal` `Ideal` `Preorder.toLT` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`Top.top` `Ideal` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`exists_le_maximal` `lt_of_lt_of_le`
`ne_top_iff_exists_maximal` 📖	mathematical	—	`Ideal` `IsMaximal` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`exists_le_maximal` `Mathlib.Tactic.Contrapose.contrapose₃` `Mathlib.Tactic.Push.not_and_eq` `top_le_iff` `IsMaximal.ne_top`
`sInf_isPrime_of_isChain` 📖	mathematical	`Set.Nonempty` `Ideal` `IsChain` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `IsPrime`	`IsPrime` `InfSet.sInf` `Ideal` `Submodule.instInfSet` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`IsPrime.ne_top` `eq_top_iff` `Eq.trans_le` `sInf_le` `mem_sInf` `Mathlib.Tactic.Push.not_forall_eq` `IsChain.total` `instReflLe` `IsPrime.mem_or_mem`
`span_singleton_lt_span_singleton` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `Preorder.toLT` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `span` `Set` `Set.instSingletonSet` `DvdNotUnit` `CommSemiring.toCommMonoidWithZero`	—	`lt_iff_le_not_ge` `span_singleton_le_span_singleton` `dvd_and_not_dvd_iff` `IsDomain.toIsCancelMulZero`
`span_singleton_prime` 📖	mathematical	—	`IsPrime` `CommSemiring.toSemiring` `span` `Set` `Set.instSingletonSet` `Prime` `CommSemiring.toCommMonoidWithZero`	—	—

Ideal.IsMaximal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coprime_of_ne` 📖	mathematical	—	`Ideal` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Top.top` `Submodule.instTop`	—	`Mathlib.Tactic.Contrapose.contrapose₂` `eq_of_le` `ne_top` `LE.le.trans_eq` `le_sup_left` `le_sup_right`
`eq_of_le` 📖	—	`Ideal` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	—	`eq_iff_le_not_lt` `out`
`exists_inv` 📖	mathematical	`Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`Ideal.isMaximal_iff` `Ideal.mem_span_insert` `Set.Subset.trans` `Set.subset_insert` `Ideal.subset_span` `Set.mem_insert` `Ideal.span_eq`
`isPrime` 📖	mathematical	—	`Ideal.IsPrime` `CommSemiring.toSemiring`	—	`out` `Set.Subset.trans` `Set.subset_insert` `Ideal.subset_span` `Set.mem_insert` `Ideal.isMaximal_iff` `Submodule.mem_span_insert` `mul_one` `mul_add` `Distrib.leftDistribClass` `mul_comm` `smul_eq_mul` `mul_assoc` `Submodule.add_mem` `Ideal.mul_mem_left` `Submodule.smul_mem` `Submodule.span_eq`
`isPrime'` 📖	mathematical	—	`Ideal.IsPrime` `CommSemiring.toSemiring`	—	`isPrime`
`lt_top` 📖	mathematical	—	`Ideal` `Preorder.toLT` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Top.top` `Submodule.instTop`	—	`Ne.lt_top` `ne_top`
`ne_top` 📖	—	—	—	—	`Ideal.isMaximal_def`
`out` 📖	mathematical	—	`IsCoatom` `Ideal` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.instOrderTop`	—	—

LinearIndependent

Definitions

Name	Category	Theorems
`Maximal` 📖	MathDef	2 math math: `Module.Basis.maximal`, `maximal_iff`

(root)

Definitions

Name	Category	Theorems
`Maximal` 📖	MathDef	105 math math: `not_maximal_subset_iff`, `MaximalFor.maximal_of_strictMonoOn`, `SimpleGraph.ConnectedComponent.maximal_connected_induce_supp`, `Matroid.isBase_compl_iff_maximal_disjoint_isBase`, `IndepMatroid.matroid_IsBase`, `OrderEmbedding.maximal_mem_image`, `minimal_mem_image_antitone_iff`, `maximal_mem_image_antitone_iff`, `MinimalFor.maximal_of_strictAntiOn`, `Maximal.dual`, `DirectedOn.maximal_iff_isGreatest`, `exists_maximal_ge_of_wellFoundedGT`, `OrderIso.image_setOf_maximal`, `OrderEmbedding.inter_preimage_setOf_maximal_eq_of_subset`, `maximal_mem_Ioc`, `maximal_true_subtype`, `isTranscendenceBasis_iff_maximal`, `maximal_false`, `SimpleGraph.isMaximalClique_iff`, `SimpleGraph.isMaximalIndepSet_compl`, `SimpleGraph.ConnectedComponent.maximal_connected_induce_iff`, `maximal_gt_iff`, `Finset.exists_le_maximal`, `image_monotone_setOf_maximal_mem`, `maximal_mem_Icc`, `maximal_iff_forall_gt`, `exists_maximal_algebraicIndependent`, `SimpleGraph.Connected.maximal_le_isAcyclic_iff_isTree`, `maximal_and_iff_left_of_imp`, `OrderEmbedding.maximal_apply_iff`, `Order.coheight_eq_coe_iff_maximal_le_coheight`, `SimpleGraph.IsMaximumIndepSet.isMaximalIndepSet`, `maximal_mem_iff`, `minimal_toDual`, `maximal_mem_image_monotone_iff`, `SimpleGraph.ConnectedComponent.maximal_connected_toSubgraph`, `Set.Finite.exists_le_maximal`, `maximal_mem_image_monotone`, `zorn_le₀`, `setOf_maximal_subset`, `Maximal.and_right`, `OrderEmbedding.maximal_mem_image_iff`, `Set.maximal_iff_forall_ssuperset`, `Set.maximal_iff_forall_insert`, `maximal_ge_iff`, `maximal_toDual`, `maximal_and_iff_right_of_imp`, `maximal_iff_eq`, `IsAntichain.maximal_mem_lowerClosure_iff_mem`, `image_antitone_setOf_maximal_mem`, `SimpleGraph.isMaximalClique_compl`, `Maximal.or`, `maximal_maximal`, `zorn_subset`, `OrderEmbedding.image_setOf_maximal`, `maximal_true`, `Ideal.exists_maximal_not_isPrincipal`, `OrderEmbedding.maximal_apply_mem_inter_range_iff`, `Finset.exists_maximal`, `Set.Subsingleton.maximal_mem_iff`, `maximal_iff_maximal_of_imp_of_forall`, `Maximal.and_left`, `Order.IsOfFiniteCharacter.exists_maximal`, `not_maximal_iff`, `image_antitone_setOf_minimal_mem`, `SimpleGraph.IsMaximumClique.isMaximalClique`, `Matroid.isBasis_iff_maximal`, `zorn_subset_nonempty`, `maximal_subset_iff`, `SimpleGraph.maximal_isAcyclic_iff_reachable_eq`, `Set.Finite.exists_maximal`, `SimpleGraph.ConnectedComponent.maximal_subgraph_connected_iff`, `zorn_le_nonempty₀`, `IsGreatest.maximal_iff`, `not_maximal_iff_exists_gt`, `SimpleGraph.maximal_isAcyclic_iff_isTree`, `SimpleGraph.isMaximalIndepSet_iff`, `IsAntichain.maximal_mem_iff`, `image_antitone_setOf_minimal`, `maximal_subtype`, `IsGreatest.maximal`, `maximal_iff`, `exists_maximal_of_wellFoundedGT`, `image_antitone_setOf_maximal`, `maximal_subset_iff'`, `maximal_eq_iff`, `Matroid.isBase_iff_maximal_indep`, `maximal_iff_isGreatest`, `SimpleGraph.exists_maximal_isAcyclic_of_le_isAcyclic`, `Minimal.of_dual`, `maximal_le_iff`, `Finset.maximal_iff_forall_insert`, `irreducibleComponents_eq_maximals_closed`, `Submonoid.IsMulSpanning.maximal_isMulPointed`, `minimal_mem_image_antitone`, `setOf_maximal_antichain`, `SimpleGraph.isTree_iff_maximal_isAcyclic`, `Maximal.mono`, `Finite.exists_le_maximal`, `AddSubmonoid.IsSpanning.maximal_isPointed`, `IsAntichain.eq_setOf_maximal`, `maximal_iff_isMax`, `image_monotone_setOf_maximal`, `OrderIso.map_maximal_mem`, `maximalFor_id`

---

← Back to Index