Commit 2026-09-30 17:48 5c302a0e

View on Github →

chore: rename LinearMap.baseChange_eq_ltensor to baseChange_eq_lTensor (#44327) Renames LinearMap.baseChange_eq_ltensor to baseChange_eq_lTensor, matching LinearMap.lTensor.

Estimated changes

Modified Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean

Modified Mathlib/LinearAlgebra/TensorProduct/Tower.lean

added theorem LinearMap.baseChange_eq_lTensor

deleted theorem LinearMap.baseChange_eq_ltensor

Modified Mathlib/RingTheory/Kaehler/JacobiZariski.lean

Modified Mathlib/RingTheory/LocalRing/Module.lean

Modified Mathlib/RingTheory/TensorProduct/Maps.lean