Theorem Algebra.TensorProduct.natCast_def'

Modification history

2023-09-27 03:37
Mathlib/RingTheory/TensorProduct.lean
chore(RingTheory/TensorProduct): extra lemmas about `{nat,int}Cast` (#7391)
Added Algebra.TensorProduct.natCast_def'View on Github →