Mathlib Map

Theorems · Definition · field theory

Semifield.toZPow

{K : Type u_2} → [self : Semifield K] → ZPow K
Defined in
Mathlib.Algebra.Field.Defs
Cited by
3 results in Mathlib
Foundations
Depth 1 from the axioms · uses no axioms
Assumes
Semifield
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Semifield.zpow_zero' · cited by 0Semifield.zpow_zero'Semifield.zpow_neg' · cited by 0Semifield.zpow_neg'Semifield.zpow_succ' · cited by 0Semifield.zpow_succ'Semifield · cited by 439SemifieldZPow · cited by 1ZPowSemifield.toZPowCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Semifieldstatement and proof · cited by 439
  • ZPowstatement · cited by 1

Cited by3

Results whose statement or proof uses this declaration.