Mathlib Map

Theorems · Theorem

not_subsingleton

∀ (α : Type u_3) [Nontrivial α], ¬Subsingleton α
Defined in
Mathlib.Logic.Nontrivial.Defs
Cited by
24 results in Mathlib
Foundations
Depth 8 from the axioms · uses no axioms
Assumes
Nontrivial
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

RingHom.injective · cited by 187RingHom.injectivebot_ne_top · cited by 24bot_ne_toptop_ne_bot · cited by 15top_ne_botCharP.ringChar_ne_one · cited by 3CharP.ringChar_ne_oneIsIsotypic.linearEquiv_fun · cited by 3IsIsotypic.linearEquiv_funMulActionWithZero.nontrivial · cited by 3MulActionWithZero.nontriv…Module.FaithfullyFlat.iff_flat_and_rTensor_faithful · cited by 2FaithfullyFlat.iff_flat_a…Function.injective_comp_right_iff_surjective · cited by 2Function.injective_comp_r…WeierstrassCurve.Affine.CoordinateRing.basis_apply · cited by 2CoordinateRing.basis_applyFunction.surjective_comp_right_iff_injective · cited by 1Function.surjective_comp_…charP_of_card_eq_prime_pow · cited by 1charP_of_card_eq_prime_powValued.integer.isPrincipalIdealRing_of_compactSpace · cited by 1integer.isPrincipalIdealR…IsIsotypicOfType.of_subsingleton · cited by 1IsIsotypicOfType.of_subsi…ZMod.subsingleton_iff · cited by 1ZMod.subsingleton_iffMonoid.one_lt_exponent · cited by 0Monoid.one_lt_exponentNontrivial · cited by 2416Nontrivialnot_nontrivial · cited by 5not_nontrivialnot_subsingletonCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by24

Results whose statement or proof uses this declaration.