Structures · Algebra
Zsqrtd.Nonsquare
A nonsquare is a natural number that is not equal to the square of an integer. This is implemented as a typeclass because it's a necessary condition for much of the Pell equation theory.
- Defined in
- Mathlib.NumberTheory.Zsqrtd.Basic
- Shape
- One type argument · adds ns
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- _private.Mathlib.NumberTheory.PellMatiyasevic.0.Pell.d
How is a type an instance?
Loading the hierarchy index…
Assumed by15
- Zsqrtd.divides_sq_eq_zero_z
- Zsqrtd.divides_sq_eq_zero
- Zsqrtd.Nonsquare.ns
- Zsqrtd.not_divides_sq
- Zsqrtd.nonneg_antisymm
- Zsqrtd.d_pos
- Zsqrtd.le_antisymm
- Zsqrtd.eq_zero_or_eq_zero_of_mul_eq_zero
- Zsqrtd.mul_pos
- Zsqrtd.add_lt_add_left
- Zsqrtd.le_of_add_le_add_left
- Zsqrtd.instNoZeroDivisorsCastInt
- Zsqrtd.instIsStrictOrderedRingCastInt
- Zsqrtd.instIsDomainCastInt
- Zsqrtd.linearOrder
Ancestors0
No ancestors.