Commit 2025-09-14 19:47 ea162bbc

View on Github →

feat: more connections between TensorProduct and map₂ (#29391) The new lemmas about map₂ are analogous to the lemmas about Set.image2.

Estimated changes

Modified Mathlib/Algebra/Lie/TensorProduct.lean

Modified Mathlib/Algebra/Module/Submodule/Bilinear.lean

added theorem Submodule.map_map₂

added theorem Submodule.map₂_map_left

added theorem Submodule.map₂_map_map

added theorem Submodule.map₂_map_right

Modified Mathlib/LinearAlgebra/TensorProduct/Basic.lean

deleted theorem TensorProduct.map_range_eq_span_tmul

added theorem TensorProduct.range_map

added theorem TensorProduct.range_map_eq_span_tmul

Modified Mathlib/LinearAlgebra/TensorProduct/Quotient.lean