ZMod p is a field

instance ZMod.instField (p : ℕ) [hp : Fact (Nat.Prime p)] : Field (ZMod p)

Field structure on ZMod p if p is prime.

Equations

• ZMod.instField p = Field.mk ⋯ zpowRec ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ (fun (x : ℚ≥0) => HMul.hMul ↑x) ⋯ ⋯ (fun (x : ℚ) => HMul.hMul ↑x) ⋯

instance ZMod.instIsDomain (p : ℕ) [hp : Fact (Nat.Prime p)] : IsDomain (ZMod p)

ZMod p is an integral domain when p is prime.