Theorem Function.Exact.comp_injective

Modification history

2024-07-10 15:00

Mathlib/Algebra/Exact.lean

feat: more API for Function.Exact (#14520) …

Modified Function.Exact.comp_injective View on Github →

2024-07-05 09:16

Mathlib/Algebra/Exact.lean

feat(RingTheory/Flat/Basic): a module is flat iff tensoring is left exact (non-categorical formulation) (#14234) …

Added Function.Exact.comp_injective View on Github →