Theorem LinearMap.baseChange_one

Modification history

2024-02-24 18:05
Mathlib/RingTheory/TensorProduct.lean
feat: Add `Module.End.baseChangeHom` (#10928) …
Added LinearMap.baseChange_oneView on Github →