Structures · Lean core
Lean.Grind.Field
A field is a commutative ring with inverses for all non-zero elements.
- Defined in
- Init.Grind.Ring.Field
- Shape
- One type argument · adds zpow, div_eq_mul_inv, zero_ne_one, inv_zero, mul_inv_cancel, zpow_zero, zpow_succ, zpow_neg
Extends3
Extended by1
Forgetful instances
Provided automatically by
Concrete types that are instances1
- Rat
How is a type an instance?
Loading the hierarchy index…
Assumed by0
No theorem or definition in Mathlib takes this class as a hypothesis.