feat(algebra/invertible): lemmas (#3493)

Coauthored by: Johan Commelin <johan@commelin.net>


Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>

src/algebra/invertible.lean

@@ -165,6 +165,15 @@ def invertible_inv {a : α} [invertible a] : invertible (a⁻¹) :=
 
 end group_with_zero
 
+/--
+Monoid homs preserve invertibility.
+-/
+def invertible.map {R : Type*} {S : Type*} [monoid R] [monoid S] (f : R →* S) (r : R) [invertible r] :
+  invertible (f r) :=
+{ inv_of := f (⅟r),
+  inv_of_mul_self := by rw [← f.map_mul, inv_of_mul_self, f.map_one],
+  mul_inv_of_self := by rw [← f.map_mul, mul_inv_of_self, f.map_one] }
+
 section ring_char
 
 /-- A natural number `t` is invertible in a field `K` if the charactistic of `K` does not divide `t`. -/
@@ -181,6 +190,10 @@ def invertible_of_char_p_not_dvd {K : Type*} [field K] {p : ℕ} [char_p K p]
   {t : ℕ} (not_dvd : ¬(p ∣ t)) : invertible (t : K) :=
 invertible_of_nonzero (λ h, not_dvd ((char_p.cast_eq_zero_iff K p t).mp h))
 
+instance invertible_of_pos {K : Type*} [field K] [char_zero K] (n : ℕ) [h : fact (0 < n)] :
+  invertible (n : K) :=
+invertible_of_nonzero $ by simpa [nat.pos_iff_ne_zero] using h
+
 end char_p
 
 section division_ring