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.
- 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 of this typeclass
- group_with_zero.to_nontrivial
- is_domain.to_nontrivial
- linear_ordered_add_comm_group_with_top.to_nontrivial
- linear_ordered_semiring.to_nontrivial
- linear_ordered_ring.to_nontrivial
- infinite.nontrivial
- division_ring.to_nontrivial
- euclidean_domain.to_nontrivial
- is_simple_order.to_nontrivial
- is_simple_group.to_nontrivial
- is_simple_add_group.to_nontrivial
- local_ring.to_nontrivial
- uniform_space.completion.nontrivial
- sort.nontrivial
- option.nontrivial
- nontrivial_prod_right
- nontrivial_prod_left
- pi.nontrivial
- function.nontrivial
- bool.nontrivial
- order_dual.nontrivial
- additive.nontrivial
- multiplicative.nontrivial
- mul_opposite.nontrivial
- add_opposite.nontrivial
- set.nontrivial_of_nonempty
- with_one.nontrivial
- with_zero.nontrivial
- with_top.nontrivial
- with_bot.nontrivial
- nat.nontrivial
- int.nontrivial
- fin.nontrivial
- finset.nontrivial
- sym.nontrivial
- rat.nontrivial
- subsemigroup.nontrivial
- add_subsemigroup.nontrivial
- submonoid.nontrivial
- add_submonoid.nontrivial
- ulift.nontrivial
- subgroup.nontrivial
- add_subgroup.nontrivial
- subsemiring_class.nontrivial
- subsemiring.nontrivial
- subring.nontrivial
- associates.nontrivial
- finsupp.nontrivial
- linear_map.module.End.nontrivial
- submodule.nontrivial
- enat.nontrivial
- cardinal.nontrivial
- monoid_algebra.nontrivial
- add_monoid_algebra.nontrivial
- polynomial.nontrivial
- ordinal.nontrivial
- ideal.nontrivial
- polynomial.subalgebra.nontrivial
- fraction_ring.nontrivial
- self_adjoint.nontrivial
- matrix.nontrivial
- free_algebra.nontrivial
- field.direct_limit.nontrivial
- category_theory.End.nontrivial
- category_theory.subobject.nontrivial
- continuous_map.nontrivial
- zmod.nontrivial
- zmod.nontrivial'
- real.nontrivial
- nonneg.nontrivial
- ennreal.nontrivial
- affine_subspace.nontrivial
- mv_power_series.nontrivial
- mv_power_series.subalgebra.nontrivial
- power_series.nontrivial
- power_series.subalgebra.nontrivial
- hahn_series.nontrivial
- hahn_series.subalgebra.nontrivial
- ratfunc.nontrivial
- algebraic_geometry.LocallyRingedSpace.component_nontrivial
- homogeneous_localization.nontrivial
- lie_submodule.nontrivial
- fractional_ideal.nontrivial
- quaternion.nontrivial
- sym_alg.nontrivial
- tropical.nontrivial
- filter.germ.nontrivial
- sym2.nontrivial
- alternating_group.nontrivial
- dihedral_group.nontrivial
- quaternion_group.nontrivial
- hamming.nontrivial
- zsqrtd.nontrivial
- lucas_lehmer.X.nontrivial
- gaussian_int.nontrivial
- ore_localization.nontrivial
- mod_p.nontrivial
- witt_vector.nontrivial
See Note [lower instance priority]
Note that since this and nonempty_of_inhabited
are the most "obvious" way to find a nonempty
instance if no direct instance can be found, we give this a higher priority than the usual 100
.
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.
Pushforward a nontrivial
instance along an injective function.
Pullback a nontrivial
instance along a surjective function.
An injective function from a nontrivial type has an argument at which it does not take a given value.
A pi type is nontrivial if it's nonempty everywhere and nontrivial somewhere.
As a convenience, provide an instance automatically if (f default)
is nontrivial.
If a different index has the non-trivial type, then use haveI := nontrivial_at that_index
.
Attempts to generate a nontrivial α
hypothesis.
The tactic first looks for an instance using apply_instance
.
If the goal is an (in)equality, the type α
is inferred from the goal.
Otherwise, the type needs to be specified in the tactic invocation, as nontriviality α
.
The nontriviality
tactic will first look for strict inequalities amongst the hypotheses,
and use these to derive the nontrivial
instance directly.
Otherwise, it will perform a case split on subsingleton α ∨ nontrivial α
, and attempt to discharge
the subsingleton
goal using simp [lemmas] with nontriviality
, where [lemmas]
is a list of
additional simp
lemmas that can be passed to nontriviality
using the syntax
nontriviality α using [lemmas]
.
example {R : Type} [ordered_ring R] {a : R} (h : 0 < a) : 0 < a :=
begin
nontriviality, -- There is now a `nontrivial R` hypothesis available.
assumption,
end
example {R : Type} [comm_ring R] {r s : R} : r * s = s * r :=
begin
nontriviality, -- There is now a `nontrivial R` hypothesis available.
apply mul_comm,
end
example {R : Type} [ordered_ring R] {a : R} (h : 0 < a) : (2 : ℕ) ∣ 4 :=
begin
nontriviality R, -- there is now a `nontrivial R` hypothesis available.
dec_trivial
end
def myeq {α : Type} (a b : α) : Prop := a = b
example {α : Type} (a b : α) (h : a = b) : myeq a b :=
begin
success_if_fail { nontriviality α }, -- Fails
nontriviality α using [myeq], -- There is now a `nontrivial α` hypothesis available
assumption
end
```