PrimeField

📁 Source: Mathlib/FieldTheory/PrimeField.lean

Statistics

Metric	Count
Definitions	0
Theorems bot_eq_of_charZero, bot_eq_of_zMod_algebra, instSubsingletonSubfieldRat, instSubsingletonSubfieldZMod	4
Total	4

Subfield

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bot_eq_of_charZero 📖	mathematical	—	Bot.bot Subfield Field.toDivisionRing OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder RingHom.fieldRange Rat.instDivisionRing algebraMap Rat.commSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DivisionRing.toRatAlgebra	—	eq_bot_iff map_bot subsingleton_iff_bot_eq_top instSubsingletonSubfieldRat RingHom.fieldRange_eq_map le_refl
bot_eq_of_zMod_algebra 📖	mathematical	—	Bot.bot Subfield Field.toDivisionRing OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder RingHom.fieldRange ZMod ZMod.instField algebraMap Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	eq_bot_iff map_bot subsingleton_iff_bot_eq_top instSubsingletonSubfieldZMod RingHom.fieldRange_eq_map le_refl

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instSubsingletonSubfieldRat 📖	mathematical	—	Subfield Rat.instDivisionRing	—	subsingleton_of_top_le_bot SubsemiringClass.instCharZero SubringClass.toSubsemiringClass SubfieldClass.toSubringClass Subfield.instSubfieldClass Rat.instCharZero Rat.subsingleton_ringHom Subtype.prop
instSubsingletonSubfieldZMod 📖	mathematical	—	Subfield ZMod Field.toDivisionRing ZMod.instField	—	subsingleton_of_top_le_bot dvd_rfl Subfield.charP ZMod.charP ZMod.subsingleton_ringHom Subtype.prop

---

← Back to Index