Theorems · Theorem · commutative algebra
Int.cast_ne_zero
∀ {α : Type u_3} [inst : AddGroupWithOne α] [CharZero α] {n : ℤ}, ↑n ≠ 0 ↔ n ≠ 0- Defined in
- Mathlib.Data.Int.Cast.Lemmas
- Cited by
- 17 results in Mathlib
- Foundations
- Depth 14 from the axioms · uses propext
- Assumes
- AddGroupWithOneCharZero
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CharZerostatement and proof · cited by 932
- AddGroupWithOnestatement and proof · cited by 111
- Int.cast_eq_zeroproof · cited by 6
Cited by17
Results whose statement or proof uses this declaration.
- Polynomial.Chebyshev.integral_eval_T_real_measureT_of_ne_zeroproof · cited by 3
- Pell.exists_of_not_isSquareproof · cited by 3
- Int.cast_div_charZeroproof · cited by 2
- Irrational.mul_intCastproof · cited by 2
- LiouvilleWith.mul_int_iffproof · cited by 2
- irrational_nrt_of_notint_nrtproof · cited by 2
- AddSubgroup.zsmul_mem_zmultiples_iff_exists_sub_divproof · cited by 2
- Irrational.div_intCastproof · cited by 1
- fourier_add_half_inv_indexproof · cited by 1
- NumberField.dedekindZeta_residue_posproof · cited by 1
- one_le_pow_mul_abs_eval_divproof · cited by 1
- Function.support_intCastproof · cited by 0