From 1f11f3f3ad6faf529ec2f1204275fbffd6a9c7fa Mon Sep 17 00:00:00 2001 From: sgouezel Date: Sat, 26 Mar 2022 19:19:53 +0000 Subject: [PATCH] chore(order/filter/basic): rename using the zero subscript convention for groups with zero (#12952) --- src/order/filter/basic.lean | 15 +++------------ 1 file changed, 3 insertions(+), 12 deletions(-) diff --git a/src/order/filter/basic.lean b/src/order/filter/basic.lean index 64f9e1d4cfd06..597993a62f7bc 100644 --- a/src/order/filter/basic.lean +++ b/src/order/filter/basic.lean @@ -1271,20 +1271,11 @@ lemma eventually_eq.inv [has_inv β] {f g : α → β} {l : filter α} (h : f = ((λ x, (f x)⁻¹) =ᶠ[l] (λ x, (g x)⁻¹)) := h.fun_comp has_inv.inv -lemma eventually_eq.div [group_with_zero β] {f f' g g' : α → β} {l : filter α} (h : f =ᶠ[l] g) - (h' : f' =ᶠ[l] g') : - ((λ x, f x / f' x) =ᶠ[l] (λ x, g x / g' x)) := -by simpa only [div_eq_mul_inv] using h.mul h'.inv - -lemma eventually_eq.div' [group β] {f f' g g' : α → β} {l : filter α} (h : f =ᶠ[l] g) +@[to_additive] +lemma eventually_eq.div [has_div β] {f f' g g' : α → β} {l : filter α} (h : f =ᶠ[l] g) (h' : f' =ᶠ[l] g') : ((λ x, f x / f' x) =ᶠ[l] (λ x, g x / g' x)) := -by simpa only [div_eq_mul_inv] using h.mul h'.inv - -lemma eventually_eq.sub [add_group β] {f f' g g' : α → β} {l : filter α} (h : f =ᶠ[l] g) - (h' : f' =ᶠ[l] g') : - ((λ x, f x - f' x) =ᶠ[l] (λ x, g x - g' x)) := -by simpa only [sub_eq_add_neg] using h.add h'.neg +h.comp₂ (/) h' @[to_additive] lemma eventually_eq.const_smul {𝕜} [has_scalar 𝕜 β] {l : filter α} {f g : α → β} (h : f =ᶠ[l] g) (c : 𝕜) :