IsSimpleOrder

📁 Source: Mathlib/Algebra/Algebra/Subalgebra/IsSimpleOrder.lean

Statistics

Metric	Count
Definitions IsSimpleOrder	1
Theorems isSimpleOrder_of_finrank_prime	1
Total	2

Subalgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSimpleOrder_of_finrank_prime 📖	mathematical	Nat.Prime Module.finrank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Semifield.toCommSemiring Ring.toSemiring	IsSimpleOrder Subalgebra Preorder.toLE PartialOrder.toPreorder instPartialOrder CompleteLattice.toBoundedOrder Algebra.instCompleteLatticeSubalgebra	—	Nat.not_prime_one bot_eq_top_iff_finrank_eq_one commRing_strongRankCondition EuclideanDomain.toNontrivial IsDomain.toNontrivial Module.Free.of_divisionRing eq_bot_of_finrank_one Algebra.toSubmodule_eq_top Submodule.eq_top_of_finrank_eq FiniteDimensional.of_finrank_pos Nat.Prime.pos finrank_toSubmodule Nat.Prime.eq_one_or_self_of_dvd Module.finrank_mul_finrank isScalarTower_mid IsScalarTower.left IsScalarTower.right IsNoetherianRing.strongRankCondition SubsemiringClass.nontrivial instSubsemiringClass PrincipalIdealRing.isNoetherianRing DivisionSemiring.isPrincipalIdealRing isDomain FiniteDimensional.finiteDimensional_subalgebra

(root)

Definitions

Name	Category	Theorems
IsSimpleOrder 📖	CompData	33 math math: isSimpleOrder_iff_isAtom_top, Ring.isField_iff_isSimpleOrder_ideal, CategoryTheory.instIsSimpleOrderSubobjectOfSimple, Subalgebra.isSimpleOrder_of_finrank, CategoryTheory.simple_iff_subobject_isSimpleOrder, IsSimpleGroup.instIsSimpleOrderSubgroup, TopologicalSpace.Opens.instIsSimpleOrderOfNonemptyOfIndiscreteTopology, isSimpleRing_iff, isSimpleOrder_iff_isSimpleOrder_orderDual, Bool.instIsSimpleOrder, Set.isSimpleOrder_Iic_iff_isAtom, Ideal.isSimpleOrder, IsSimpleAddGroup.instIsSimpleOrderAddSubgroup, IsSimpleRing.simple, isSimpleModule_iff, MulAction.isSimpleOrder_blockMem_iff_isPreprimitive, isSimpleOrder_iff, Prop.instIsSimpleOrderProp, isSimpleOrder_iff_isCoatom_bot, AffineSubspace.instIsSimpleOrderOfSubsingleton, AddAction.isSimpleOrder_blockMem_iff_isPreprimitive, OrderIso.isSimpleOrder_iff, instIsSimpleOrderIdeal, RootPairing.isIrreducible_iff_invtRootSubmodule, is_simple_module_of_finrank_eq_one, IsSimpleModule.toIsSimpleOrder, Subalgebra.isSimpleOrder_of_finrank_prime, Order.krullDim_eq_one_iff_of_boundedOrder, IntermediateField.isSimpleOrder_of_finrank_prime, Set.isSimpleOrder_Ici_iff_isCoatom, OrderIso.isSimpleOrder, IsSimpleOrder.of_forall_eq_top, OrderDual.instIsSimpleOrder

---

← Back to Index