Theorem IsAddUnit.tmul_left

Modification history

2026-02-12 09:07
Mathlib/LinearAlgebra/TensorProduct/Basic.lean
refactor(LinearAlgebra/TensorProduct): split large file (#34798) …
Modified IsAddUnit.tmul_leftView on Github →
2025-09-20 08:39
Mathlib/LinearAlgebra/TensorProduct/Basic.lean
feat(Algebra): preliminaries for ring structure on `AddLocalization` (#29597)
Added IsAddUnit.tmul_leftView on Github →