Nontrivial types
A type is nontrivial if it contains at least two elements. This is useful in particular for rings (where it is equivalent to the fact that zero is different from one) and for vector spaces (where it is equivalent to the fact that the dimension is positive).
We introduce a typeclass nontrivial formalizing this property.
@[class]
- exists_pair_ne : ∃ (x y : α), x ≠ y
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.
Instances
- group_with_zero.to_nontrivial
- domain.to_nontrivial
- linear_ordered_semiring.to_nontrivial
- ordered_ring.to_nontrivial
- nonneg_ring.to_nontrivial
- canonically_ordered_comm_semiring.to_nontrivial
- with_top.nontrivial
- division_ring.to_nontrivial
- field.to_nontrivial
- euclidean_domain.to_nontrivial
- local_ring.to_nontrivial
- nontrivial_prod_left
- nontrivial_prod_right
- option.nontrivial
- function.nontrivial
- with_one.nontrivial
- with_zero.nontrivial
- nat.nontrivial
- opposite.nontrivial
- int.nontrivial
- rat.nontrivial
- associates.nontrivial
- subsemiring.nontrivial
- subalgebra.nontrivial
- polynomial.nontrivial
- cardinal.nontrivial
- ordinal.nontrivial
- field.direct_limit.nontrivial
- real.nontrivial
- filter.germ.nontrivial
- zmod.nontrivial
- zsqrtd.nontrivial
- gaussian_int.nontrivial
- lucas_lehmer.X.nontrivial
- ring.fractional_ideal.nontrivial
- mv_power_series.nontrivial
- power_series.nontrivial
@[instance]
Equations
- nontrivial.to_nonempty = _
- _ = _
An inhabited type is either nontrivial, or has a unique element.
Equations
- nontrivial_psum_unique α = dite (nontrivial α) (λ (h : nontrivial α), psum.inl h) (λ (h : ¬nontrivial α), psum.inr {to_inhabited := {default := inhabited.default α _inst_1}, uniq := _})
A type is either a subsingleton or nontrivial.
@[instance]
def
nontrivial_prod_left
{α : Type u_1}
{β : Type u_2}
[nontrivial α]
[nonempty β] :
nontrivial (α × β)
Equations
@[instance]
def
nontrivial_prod_right
{α : Type u_1}
{β : Type u_2}
[nontrivial α]
[nonempty β] :
nontrivial (β × α)
Equations
@[instance]
Equations
@[instance]
def
function.nontrivial
{α : Type u_1}
{β : Type u_2}
[nonempty α]
[nontrivial β] :
nontrivial (α → β)
Equations
theorem
function.injective.nontrivial
{α : Type u_1}
{β : Type u_2}
[nontrivial α]
{f : α → β} :
function.injective f → nontrivial β
Pushforward a nontrivial instance along an injective function.
Pullback a nontrivial instance along a surjective function.