Structures · Logic and sets
Nontrivial
Predicate typeclass for expressing that a type is not reduced to a single element. In rings,
this is equivalent to 0 ≠ 1. In vector spaces, this is equivalent to positive dimension.
- Defined in
- Mathlib.Logic.Nontrivial.Defs
- Shape
- One type argument · adds exists_pair_ne
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by11
Forgetful instances
Concrete types that are instances100
- Int
- Nat
- Real
- Rat
- Bool
- Complex
- SeparationQuotient
- NNReal
- ContinuousLinearMap
- ZMod
- ENNReal
- Polynomial
- Filter.Germ
- CStarMatrix
- CommRingCat.carrier
- RatFunc
- UniformSpace.Completion
- NNRat
- TensorProduct
- Quaternion
- Unitization
- FractionRing
- WithConv
- Matrix
- HahnSeries
- NonemptyInterval
- LocallyConstant
- ENat
- QuadraticAlgebra
- Units
- WithLp
- FreeAbelianGroup
- EReal
- MonoidAlgebra
- TrivSqZeroExt
- ModuleCat.carrier
- AddMonoidAlgebra
- DirectLimit
- Finsupp
- Zsqrtd
- ZNum
- SymAlg
- Localization
- SkewMonoidAlgebra
- Interval
- CauSeq.Completion.Cauchy
- PerfectClosure
- OreLocalization
- QuaternionAlgebra
- WittVector
- NumberField.InfiniteAdeleRing
- TopologicalSpace.NonemptyCompacts
- NumberField.RingOfIntegers
- LucasLehmer.X
- CategoryTheory.End
- GaussianInt
- WithCStarModule
- Tropical
- MvPowerSeries
- FreeRing
- Ordinal
- FractionalIdeal
- Ring.NormalClosure
- Module.End
- Cardinal
- CliffordAlgebra
- SymmetricAlgebra
- LieSubmodule
- Ring.DirectLimit
- Associates
- SimpleGraph
- FreeAlgebra
- FreeGroup
- TopologicalSpace.Opens
- FreeAddGroup
- TopologicalSpace.Compacts
- Hamming
- TensorAlgebra
- Digraph
- Equiv.Perm
- PolynomialModule
- AddSubgroup
- ArchimedeanClass
- NumberField.mixedEmbedding.euclidean.mixedSpace
- SkewPolynomial
- Sym2
- AddSubmonoid
- MvPolynomial
- Sym
- RingCon
- ValuationRing.ValueGroup
- DihedralGroup
- QuaternionGroup
- MulArchimedeanClass
- AddLocalization
- TwoSidedIdeal
- UpperHalfPlane
- AffineSubspace
- CategoryTheory.Subobject
- OrderType
How is a type an instance?
Loading the hierarchy index…
Assumed by1,875
- cfcₙ
- RingHom.injective
- Nat.cast_pos
- exists_ne
- Units.ne_zero
- cfcₙHom
- Polynomial.Monic.ne_zero
- Module.finrank_pos
- Finset.prod_ne_zero_iff
- minpoly.ne_zero
- Polynomial.natDegree_X
- mem_nonZeroDivisors_iff_ne_zero
- IsUnit.ne_zero
- FractionalIdeal.dual
- exists_pair_ne
- cfcₙ_apply
- cfcₙ_apply_of_not_predicate
- Polynomial.degree_modByMonic_lt
- Finset.prod_pos
- cfcₙ_congr
- bot_ne_top
- not_subsingleton
- Polynomial.natDegree_X_sub_C
- Polynomial.map_ne_zero
- nonZeroDivisors.ne_zero
- AffineIndependent.injective
- LinearIndependent.injective
- Polynomial.Monic.natDegree_map
- Polynomial.X_sub_C_ne_zero
- Polynomial.natDegree_map
- not_isUnit_zero
- LinearIndependent.ne_zero
- map_ne_zero
- RingHom.domain_nontrivial
- cfcₙ_id
- isAlgebraic_algebraMap
- AlgEquiv.ofInjectiveField
- Squarefree.ne_zero
- finrank_bot
- Fintype.one_lt_card
- IsIntegral.isAlgebraic
- nonZeroDivisors.coe_ne_zero
- Module.nontrivial
- Function.Injective.nontrivial
- LinearIndependent.cardinal_lift_le_rank
- Polynomial.X_pow_sub_C_ne_zero
- Polynomial.degree_X_pow
- cfcₙ_apply_of_not_map_zero
- top_ne_bot
- Polynomial.degree_X_pow_sub_C