Theorems · Theorem · commutative algebra
Int.commute_cast
∀ {α : Type u_3} [inst : NonAssocRing α] (a : α) (n : ℤ), Commute a ↑n- Defined in
- Mathlib.Data.Int.Cast.Lemmas
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 17 from the axioms · uses propext
- Assumes
- NonAssocRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Commutestatement · cited by 639
- NonAssocRingstatement and proof · cited by 483
- Commute.symmproof · cited by 79
- Int.cast_commuteproof · cited by 7
Cited by5
Results whose statement or proof uses this declaration.
- Rat.cast_mul_of_ne_zeroproof · cited by 1
- Rat.cast_div_of_ne_zeroproof · cited by 0
- Set.intCast_mem_centerproof · cited by 0
- SemiconjBy.intCast_mul_rightproof · cited by 0
- Commute.intCast_rightproof · cited by 0