From 63315a3ffa29e93624c62bba63d4e84e1dc8e136 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Sat, 7 Nov 2020 18:41:18 +0000 Subject: [PATCH] fix(*): Lemma rename --- src/algebra/pointwise.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/algebra/pointwise.lean b/src/algebra/pointwise.lean index 7a447d925a9e4..300fadb5b8f33 100644 --- a/src/algebra/pointwise.lean +++ b/src/algebra/pointwise.lean @@ -365,7 +365,7 @@ by simp only [← image_smul, image_eta, zero_smul, h.image_const, singleton_zer lemma mem_inv_smul_set_iff [field α] [mul_action α β] {a : α} (ha : a ≠ 0) (A : set β) (x : β) : x ∈ a⁻¹ • A ↔ a • x ∈ A := -by simp only [← image_smul, mem_image, inv_smul_eq_iff ha, exists_eq_right] +by simp only [← image_smul, mem_image, inv_smul_eq_iff' ha, exists_eq_right] lemma mem_smul_set_iff_inv_smul_mem [field α] [mul_action α β] {a : α} (ha : a ≠ 0) (A : set β) (x : β) : x ∈ a • A ↔ a⁻¹ • x ∈ A :=