Skip to content

Commit bc1ba61

Browse files
committed
chore(Data/Setoid/Basic): abbrev kerLift -> def kerLift
1 parent cf13cfd commit bc1ba61

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

Mathlib/Data/Setoid/Basic.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -317,7 +317,7 @@ theorem lift_unique {r : Setoid α} {f : α → β} (H : r ≤ ker f) (g : Quoti
317317
rw [← Quotient.mk, Quotient.lift_mk f H, Hg, Function.comp_apply, Quotient.mk''_eq_mk]
318318

319319
/-- Given a function `f`, lift it to the quotient by its kernel. -/
320-
abbrev kerLift (f : α → β) : Quotient (ker f) → β := Quotient.lift f fun _ _ => id
320+
def kerLift (f : α → β) : Quotient (ker f) → β := Quotient.lift f fun _ _ => id
321321

322322
@[simp]
323323
theorem kerLift_mk (f : α → β) (x : α) : kerLift f ⟦x⟧ = f x := rfl

0 commit comments

Comments
 (0)