Last active
April 23, 2020 12:38
-
-
Save Vierkantor/e73209684c16b725e29880de7443c9f2 to your computer and use it in GitHub Desktop.
invertible.lean (WIP)
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| import tactic | |
| universes u | |
| variables {α : Type u} | |
| /-- `invertible a` gives a two-sided multiplicative inverse of `a` -/ | |
| class invertible [has_mul α] [has_one α] (a : α) : Type u := | |
| (inv_of : α) (inv_of_mul_self : inv_of * a = 1) (mul_inv_of_self : a * inv_of = 1) | |
| -- This notation has the same precedence as `has_inv.inv`. | |
| notation `⅟`:1034 := invertible.inv_of | |
| @[simp] | |
| lemma inv_of_mul_self [has_mul α] [has_one α] (a : α) [invertible a] : ⅟ a * a = 1 := | |
| invertible.inv_of_mul_self | |
| @[simp] | |
| lemma mul_inv_of_self [has_mul α] [has_one α] (a : α) [invertible a] : a * ⅟ a = 1 := | |
| invertible.mul_inv_of_self | |
| @[simp] | |
| lemma mul_inv_of_mul_self_cancel [monoid α] (a b : α) [invertible b] : a * ⅟ b * b = a := | |
| by simp [mul_assoc] | |
| @[simp] | |
| lemma mul_mul_inv_of_self_cancel [monoid α] (a b : α) [invertible b] : a * b * ⅟ b = a := | |
| by simp [mul_assoc] | |
| lemma left_inv_eq_right_inv [monoid α] {a b c : α} (hba : b * a = 1) (hac : a * c = 1) : b = c := | |
| by rw [←one_mul c, ←hba, mul_assoc, hac, mul_one b] | |
| instance [monoid α] (a : α) : subsingleton (invertible a) := | |
| ⟨ λ ⟨b, hba, hab⟩ ⟨c, hca, hac⟩, by { congr, exact left_inv_eq_right_inv hba hac } ⟩ | |
| lemma is_unit_of_invertible [monoid α] (a : α) [invertible a] : is_unit a := | |
| ⟨⟨a, ⅟ a, mul_inv_of_self a, inv_of_mul_self a⟩, rfl⟩ | |
| @[priority(100)] | |
| instance invertible_of_group [group α] (a : α) : invertible a := | |
| ⟨a⁻¹, inv_mul_self a, mul_inv_self a⟩ | |
| @[simp] lemma inv_of_eq_group_inv [group α] (a : α) : ⅟ a = a⁻¹ := | |
| rfl | |
| instance invertible_one [monoid α] : invertible (1 : α) := | |
| ⟨ 1, mul_one _, one_mul _ ⟩ | |
| instance invertible_neg [ring α] {a : α} [invertible a] : invertible (-a) := | |
| ⟨ -⅟a, by simp, by simp ⟩ | |
| instance invertible_inv_of [has_one α] [has_mul α] {a : α} [invertible a] : invertible (⅟ a) := | |
| ⟨ a, mul_inv_of_self a, inv_of_mul_self a ⟩ | |
| instance invertible_mul [monoid α] (a b : α) [invertible a] [invertible b] : invertible (a * b) := | |
| ⟨ ⅟b * ⅟a, by simp [←mul_assoc], by simp [←mul_assoc] ⟩ | |
| section division_ring | |
| variable [division_ring α] | |
| lemma nonzero_of_invertible (a : α) [invertible a] : a ≠ 0 := | |
| λ ha, zero_ne_one $ calc 0 = ⅟ a * a : by simp [ha] | |
| ... = 1 : inv_of_mul_self a | |
| /-- `a⁻¹` is an inverse of `a` if `a ≠ 0` -/ | |
| def invertible_of_nonzero {a : α} (h : a ≠ 0) : invertible a := | |
| ⟨ a⁻¹, inv_mul_cancel h, mul_inv_cancel h ⟩ | |
| @[simp] lemma inv_of_eq_division_ring_inv (a : α) [invertible a] : ⅟ a = a⁻¹ := | |
| left_inv_eq_right_inv (inv_of_mul_self a) (mul_inv_cancel (nonzero_of_invertible a)) | |
| @[simp] lemma inv_mul_cancel_of_invertible (a : α) [invertible a] : a⁻¹ * a = 1 := | |
| inv_mul_cancel (nonzero_of_invertible a) | |
| @[simp] lemma mul_inv_cancel_of_invertible (a : α) [invertible a] : a * a⁻¹ = 1 := | |
| mul_inv_cancel (nonzero_of_invertible a) | |
| @[simp] lemma div_mul_cancel_of_invertible (a b : α) [invertible b] : a / b * b = a := | |
| div_mul_cancel a (nonzero_of_invertible b) | |
| @[simp] lemma mul_div_cancel_of_invertible (a b : α) [invertible b] : a * b / b = a := | |
| mul_div_cancel a (nonzero_of_invertible b) | |
| @[simp] lemma div_self_of_invertible (a : α) [invertible a] : a / a = 1 := | |
| div_self (nonzero_of_invertible a) | |
| instance invertible_div (a b : α) [invertible a] [invertible b] : invertible (a / b) := | |
| ⟨ b / a, by simp [←mul_div_assoc], by simp [←mul_div_assoc] ⟩ | |
| instance invertible_inv {a : α} [invertible a] : invertible (a⁻¹) := | |
| ⟨ a, by simp, by simp ⟩ | |
| instance invertible_succ [char_zero α] (n : ℕ) : invertible (n.succ : α) := | |
| invertible_of_nonzero (nat.cast_ne_zero.mpr (nat.succ_ne_zero _)) | |
| instance invertible_two [char_zero α] : invertible (2 : α) := | |
| invertible_of_nonzero (by exact_mod_cast (dec_trivial : 2 ≠ 0)) | |
| instance invertible_three [char_zero α] : invertible (3 : α) := | |
| invertible_of_nonzero (by exact_mod_cast (dec_trivial : 3 ≠ 0)) | |
| -- Feel free to add your own numbers here... | |
| end division_ring |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment