Theorem Setoid.lift_injective_iff_ker_eq_of_le

Modification history

2025-11-04 17:16
Mathlib/Data/Setoid/Basic.lean
feat(Data/Setoid/Basic): add theorems about lifting a function to its kernel (#28818) …
Added Setoid.lift_injective_iff_ker_eq_of_leView on Github →