feat(data/polynomial): lemmas about map (#530)

leanprover-community · Jan 9, 2019 · d0532c1 · d0532c1
1 parent 2e63635
commit d0532c1
Show file tree

Hide file tree

Showing 3 changed files with 213 additions and 31 deletions.
diff --git a/algebra/field.lean b/algebra/field.lean
@@ -199,6 +199,12 @@ by rw [mul_inv_cancel ((map_ne_zero f).2 h), ← map_mul f, mul_inv_cancel h, ma
 lemma map_div' (h : y ≠ 0) : f (x / y) = f x / f y :=
 (map_mul f).trans $ congr_arg _ $ map_inv' f h
 
+lemma injective : function.injective f :=
+(is_add_group_hom.injective_iff _).2
+  (λ a ha, classical.by_contradiction $ λ ha0,
+    by simpa [ha, is_ring_hom.map_mul f, is_ring_hom.map_one f, zero_ne_one]
+        using congr_arg f (mul_inv_cancel ha0))
+
 end
 
 section

diff --git a/algebra/group.lean b/algebra/group.lean
@@ -708,6 +708,14 @@ protected lemma is_conj (f : α → β) [is_group_hom f] {a b : α} : is_conj a
 lemma to_is_monoid_hom (f : α → β) [is_group_hom f] : is_monoid_hom f :=
 ⟨is_group_hom.one f, is_group_hom.mul f⟩
 
+@[to_additive is_add_group_hom.injective_iff]
+lemma injective_iff (f : α → β) [is_group_hom f] :
+  function.injective f ↔ (∀ a, f a = 1 → a = 1) :=
+⟨λ h _, by rw ← is_group_hom.one f; exact @h _ _,
+  λ h x y hxy, by rw [← inv_inv (f x), inv_eq_iff_mul_eq_one, ← is_group_hom.inv f,
+      ← is_group_hom.mul f] at hxy;
+    simpa using inv_eq_of_mul_eq_one (h _ hxy)⟩
+
 attribute [instance] is_group_hom.to_is_monoid_hom
   is_add_group_hom.to_is_add_monoid_hom