Theorem Module.Flat.iff_rTensor_injective'

Modification history

2025-09-28 10:35
Mathlib/RingTheory/Flat/Basic.lean
chore(RingTheory/Flat): split CharacterModule results from `Flat/Basic.lean` (#29808) …
Modified Module.Flat.iff_rTensor_injective'View on Github →
2023-11-19 22:31
Mathlib/RingTheory/Flat.lean
Extend RingTheory.Flat.iff_rTensor_injective to all ideals (#8494) …
Added Module.Flat.iff_rTensor_injective'View on Github →