Commit 2025-08-18 11:37 038570e0

View on Github →

feat(RingTheory): IsTensorProduct versions of the lemmas about tensoring with a flat module preserves injections (#27757) Add some lemmas about IsTensorProduct and the IsTensorProduct versions of the lemmas about tensoring with a flat module preserves injections.

Estimated changes

Modified Mathlib/RingTheory/Flat/Basic.lean

added theorem IsTensorProduct.map_id_injective_of_flat_left

added theorem IsTensorProduct.map_id_injective_of_flat_right

added theorem IsTensorProduct.map_injective_of_flat_left_right

added theorem IsTensorProduct.map_injective_of_flat_right_left

Modified Mathlib/RingTheory/IsTensorProduct.lean

modified theorem IsTensorProduct.equiv_symm_apply

modified theorem IsTensorProduct.equiv_toLinearMap

modified theorem IsTensorProduct.inductionOn

modified theorem IsTensorProduct.lift_eq

added theorem IsTensorProduct.map_comp

modified theorem IsTensorProduct.map_eq

added theorem IsTensorProduct.map_id

added theorem IsTensorProduct.map_map

modified theorem IsTensorProduct.of_equiv