Theorem Algebra.TensorProduct.intCast_def'

Modification history

2025-08-20 00:04

Mathlib/RingTheory/TensorProduct/Basic.lean

chore(TensorProduct): group structure from the first factor only (#28660) …

Modified Algebra.TensorProduct.intCast_def'View on Github →

2023-09-27 03:37

Mathlib/RingTheory/TensorProduct.lean

chore(RingTheory/TensorProduct): extra lemmas about `{nat,int}Cast` (#7391)

Added Algebra.TensorProduct.intCast_def'View on Github →