Skip to content

Commit

Permalink
fix(*): Lemma rename
Browse files Browse the repository at this point in the history
  • Loading branch information
eric-wieser committed Nov 7, 2020
1 parent b3fcb08 commit 63315a3
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/algebra/pointwise.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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 :=
Expand Down

0 comments on commit 63315a3

Please sign in to comment.