Mathlib Map

Theorems · Theorem · commutative algebra

one_ne_zero

∀ {α : Type u_2} [inst : Zero α] [inst_1 : One α] [NeZero 1], 1 ≠ 0
Defined in
Mathlib.Algebra.NeZero
Cited by
885 results in Mathlib
Foundations
Depth 6 from the axioms, rests on 14 definitions · uses no axioms
Assumes
ZeroOneNeZero
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

one_ne_zero' · cited by 23one_ne_zero'LinearIndependent.injective · cited by 21LinearIndependent.injecti…Polynomial.Monic.natDegree_map · cited by 21Monic.natDegree_mapmap_ne_zero · cited by 20map_ne_zeroComplex.cpow_one · cited by 20Complex.cpow_oneMeasureTheory.eLpNorm_one_eq_lintegral_enorm · cited by 16MeasureTheory.eLpNorm_one…Polynomial.degree_one · cited by 14Polynomial.degree_onedifferentiableWithinAt_localInvariantProp · cited by 13differentiableWithinAt_lo…affineCombination_mem_affineSpan · cited by 12affineCombination_mem_aff…Complex.Gamma_add_one · cited by 12Complex.Gamma_add_oneENNReal.one_rpow · cited by 12ENNReal.one_rpowAbsoluteValue.map_one · cited by 11AbsoluteValue.map_oneModule.Basis.injective · cited by 11Basis.injectivePolynomial.monic_X_add_C · cited by 9Polynomial.monic_X_add_CFinset.prod_eq_zero_iff · cited by 9Finset.prod_eq_zero_iffone_ne_zeroCITED BYCITES

Cites0

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

Nothing in Mathlib beyond the foundations.

Cited by885

Results whose statement or proof uses this declaration.

Showing the 200 most cited of 885.