feat(ring_theory/fintype): in a finite nonzero_semiring, fintype.card (units R) < fintype.card R (#2793)

Author: kim-em

src/algebra/associated.lean

@@ -18,7 +18,7 @@ variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*}
   refine ⟨⟨0, 0, _, _⟩, rfl⟩; apply subsingleton.elim
  end⟩
 
-@[simp] theorem not_is_unit_zero [nonzero_comm_ring α] : ¬ is_unit (0 : α) :=
+@[simp] theorem not_is_unit_zero [nonzero_semiring α] : ¬ is_unit (0 : α) :=
 mt is_unit_zero_iff.1 zero_ne_one
 
 lemma is_unit_pow [monoid α] {a : α} (n : ℕ) : is_unit a → is_unit (a ^ n) :=
@@ -50,7 +50,7 @@ theorem is_unit_of_dvd_unit {α} [comm_semiring α] {x y : α}
 is_unit_iff_dvd_one.2 $ dvd_trans xy $ is_unit_iff_dvd_one.1 hu
 
 theorem is_unit_int {n : ℤ} : is_unit n ↔ n.nat_abs = 1 :=
-⟨λ ⟨u, hu⟩, (int.units_eq_one_or u).elim (by simp *) (by simp *),
+⟨begin rintro ⟨u, rfl⟩, exact (int.units_eq_one_or u).elim (by simp) (by simp) end,
   λ h, is_unit_iff_dvd_one.2 ⟨n, by rw [← int.nat_abs_mul_self, h]; refl⟩⟩
 
 lemma is_unit_of_dvd_one [comm_semiring α] : ∀a ∣ 1, is_unit (a:α)
@@ -201,7 +201,7 @@ theorem unit_associated_one [monoid α] {u : units α} : (u : α) ~ᵤ 1 := ⟨u
 
 theorem associated_one_iff_is_unit [monoid α] {a : α} : (a : α) ~ᵤ 1 ↔ is_unit a :=
 iff.intro
-  (assume h, let ⟨c, h⟩ := h.symm in h ▸ ⟨c, one_mul _⟩)
+  (assume h, let ⟨c, h⟩ := h.symm in h ▸ ⟨c, (one_mul _).symm⟩)
   (assume ⟨c, h⟩, associated.symm ⟨c, by simp [h]⟩)
 
 theorem associated_zero_iff_eq_zero [comm_semiring α] (a : α) : a ~ᵤ 0 ↔ a = 0 :=
@@ -267,7 +267,7 @@ by haveI := classical.dec; exact not_iff_not.2 (eq_zero_iff_of_associated h)
 lemma prime_of_associated [comm_semiring α] {p q : α} (h : p ~ᵤ q) (hp : prime p) : prime q :=
 ⟨(ne_zero_iff_of_associated h).1 hp.ne_zero,
   let ⟨u, hu⟩ := h in
-    ⟨λ ⟨v, hv⟩, hp.not_unit ⟨v * u⁻¹, by simp [hv.symm, hu.symm]⟩,
+    ⟨λ ⟨v, hv⟩, hp.not_unit ⟨v * u⁻¹, by simp [hv, hu.symm]⟩,
       hu ▸ by { simp [mul_unit_dvd_iff], intros a b, exact hp.div_or_div }⟩⟩
 
 lemma prime_iff_of_associated [comm_semiring α] {p q : α}
@@ -285,7 +285,7 @@ lemma irreducible_of_associated [comm_semiring α] {p q : α} (h : p ~ᵤ q)
   have hpab : p = a * (b * (u⁻¹ : units α)),
     from calc p = (p * u) * (u ⁻¹ : units α) : by simp
       ... = _ : by rw hu; simp [hab, mul_assoc],
-  (hp.2 _ _ hpab).elim or.inl (λ ⟨v, hv⟩, or.inr ⟨v * u, by simp [hv.symm]⟩)⟩
+  (hp.2 _ _ hpab).elim or.inl (λ ⟨v, hv⟩, or.inr ⟨v * u, by simp [hv]⟩)⟩
 
 lemma irreducible_iff_of_associated [comm_semiring α] {p q : α} (h : p ~ᵤ q) :
   irreducible p ↔ irreducible q :=
@@ -399,7 +399,7 @@ theorem coe_unit_eq_one : ∀u:units (associates α), (u : associates α) = 1
 
 theorem is_unit_iff_eq_one (a : associates α) : is_unit a ↔ a = 1 :=
 iff.intro
-  (assume ⟨u, h⟩, h.symm ▸ coe_unit_eq_one _)
+  (assume ⟨u, h⟩, h ▸ coe_unit_eq_one _)
   (assume h, h.symm ▸ is_unit_one)
 
 theorem is_unit_mk {a : α} : is_unit (associates.mk a) ↔ is_unit a :=

src/algebra/gcd_domain.lean

@@ -64,7 +64,7 @@ lemma normalize_eq_zero {x : α} : normalize x = 0 ↔ x = 0 :=
 ⟨λ hx, (associated_zero_iff_eq_zero x).1 $ hx ▸ associated_normalize, by rintro rfl; exact normalize_zero⟩
 
 lemma normalize_eq_one {x : α} : normalize x = 1 ↔ is_unit x :=
-⟨λ hx, is_unit_iff_exists_inv.2 ⟨_, hx⟩, λ ⟨u, hu⟩, hu.symm ▸ normalize_coe_units u⟩
+⟨λ hx, is_unit_iff_exists_inv.2 ⟨_, hx⟩, λ ⟨u, hu⟩, hu ▸ normalize_coe_units u⟩
 
 theorem norm_unit_mul_norm_unit (a : α) : norm_unit (a * norm_unit a) = 1 :=
 classical.by_cases (assume : a = 0, by simp only [this, norm_unit_zero, zero_mul]) $

src/algebra/group/units.lean

@@ -202,7 +202,7 @@ variables {M : Type*} {N : Type*}
 The actual definition says that `a` is equal to some `u : units M`, where
 `units M` is a bundled version of `is_unit`. -/
 @[to_additive is_add_unit "An element `a : M` of an add_monoid is an `add_unit` if it has a two-sided additive inverse. The actual definition says that `a` is equal to some `u : add_units M`, where `add_units M` is a bundled version of `is_add_unit`."]
-def is_unit [monoid M] (a : M) : Prop := ∃ u : units M, a = u
+def is_unit [monoid M] (a : M) : Prop := ∃ u : units M, (u : M) = a
 
 @[simp, to_additive is_add_unit_add_unit]
 lemma is_unit_unit [monoid M] (u : units M) : is_unit (u : M) := ⟨u, rfl⟩
@@ -229,9 +229,9 @@ theorem units.is_unit_mul_units [monoid M] (a : M) (u : units M) :
   is_unit (a * u) ↔ is_unit a :=
 iff.intro
   (assume ⟨v, hv⟩,
-    have is_unit (a * ↑u * ↑u⁻¹), by existsi v * u⁻¹; rw [hv, units.coe_mul],
+    have is_unit (a * ↑u * ↑u⁻¹), by existsi v * u⁻¹; rw [←hv, units.coe_mul],
     by rwa [mul_assoc, units.mul_inv, mul_one] at this)
-  (assume ⟨v, hv⟩, hv.symm ▸ ⟨v * u, (units.coe_mul v u).symm⟩)
+  (assume ⟨v, hv⟩, hv ▸ ⟨v * u, (units.coe_mul v u).symm⟩)
 
 @[to_additive is_add_unit_of_add_is_add_unit_left]
 theorem is_unit_of_mul_is_unit_left [comm_monoid M] {x y : M}
@@ -245,10 +245,10 @@ is_unit_iff_exists_inv.2 ⟨y * z, by rwa ← mul_assoc⟩
 
 @[to_additive] theorem is_unit.mul_right_inj [monoid M] {a b c : M} (ha : is_unit a) :
   a * b = a * c ↔ b = c :=
-by cases ha with a ha; rw [ha, units.mul_right_inj]
+by cases ha with a ha; rw [←ha, units.mul_right_inj]
 
 @[to_additive] theorem is_unit.mul_left_inj [monoid M] {a b c : M} (ha : is_unit a) :
   b * a = c * a ↔ b = c :=
-by cases ha with a ha; rw [ha, units.mul_left_inj]
+by cases ha with a ha; rw [←ha, units.mul_left_inj]
 
 end is_unit

src/algebra/group/units_hom.lean

@@ -94,7 +94,7 @@ to `f : M →* units N`. See also `units.lift_right` for a computable version. -
 @[to_additive "If a homomorphism `f : M →+ N` sends each element to an `is_add_unit`, then it can be lifted to `f : M →+ add_units N`. See also `add_units.lift_right` for a computable version."]
 noncomputable def is_unit.lift_right [monoid M] [monoid N] (f : M →* N)
   (hf : ∀ x, is_unit (f x)) : M →* units N :=
-units.lift_right f (λ x, classical.some (hf x)) $ λ x, (classical.some_spec (hf x)).symm
+units.lift_right f (λ x, classical.some (hf x)) $ λ x, classical.some_spec (hf x)
 
 @[to_additive] lemma is_unit.coe_lift_right [monoid M] [monoid N] (f : M →* N)
   (hf : ∀ x, is_unit (f x)) (x) :
@@ -103,10 +103,10 @@ units.coe_lift_right _ x
 
 @[simp, to_additive] lemma is_unit.mul_lift_right_inv [monoid M] [monoid N] (f : M →* N)
   (h : ∀ x, is_unit (f x)) (x) : f x * ↑(is_unit.lift_right f h x)⁻¹ = 1 :=
-units.mul_lift_right_inv (λ y, (classical.some_spec $ h y).symm) x
+units.mul_lift_right_inv (λ y, classical.some_spec $ h y) x
 
 @[simp, to_additive] lemma is_unit.lift_right_inv_mul [monoid M] [monoid N] (f : M →* N)
   (h : ∀ x, is_unit (f x)) (x) : ↑(is_unit.lift_right f h x)⁻¹ * f x = 1 :=
-units.lift_right_inv_mul (λ y, (classical.some_spec $ h y).symm) x
+units.lift_right_inv_mul (λ y, classical.some_spec $ h y) x
 
 end is_unit

src/algebra/group_with_zero.lean

@@ -235,7 +235,7 @@ variables {G₀ : Type*} [group_with_zero G₀]
 lemma is_unit.mk0 (x : G₀) (hx : x ≠ 0) : is_unit x := is_unit_unit (units.mk0 x hx)
 
 lemma is_unit_iff_ne_zero {x : G₀} : is_unit x ↔ x ≠ 0 :=
-⟨λ ⟨u, hu⟩, hu.symm ▸ λ h : u.1 = 0, by simpa [h, zero_ne_one] using u.3, is_unit.mk0 x⟩
+⟨λ ⟨u, hu⟩, hu ▸ λ h : u.1 = 0, by simpa [h, zero_ne_one] using u.3, is_unit.mk0 x⟩
 
 lemma mul_eq_zero' (a b : G₀) (h : a * b = 0) : a = 0 ∨ b = 0 :=
 begin

src/algebra/ring.lean

@@ -7,7 +7,6 @@ import algebra.group.hom
 import algebra.group.units
 import tactic.norm_cast
 import tactic.split_ifs
-import algebra.group.units
 
 /-!
 # Properties and homomorphisms of semirings and rings
@@ -942,11 +941,11 @@ variables [semiring α]
 
 theorem mul_left_eq_zero_iff_eq_zero {r u : α}
   (hu : is_unit u) : r * u = 0 ↔ r = 0 :=
-by cases hu with u hu; exact hu.symm ▸ units.mul_left_eq_zero_iff_eq_zero u
+by cases hu with u hu; exact hu ▸ units.mul_left_eq_zero_iff_eq_zero u
 
 theorem mul_right_eq_zero_iff_eq_zero {r u : α}
   (hu : is_unit u) : u * r = 0 ↔ r = 0 :=
-by cases hu with u hu; exact hu.symm ▸ units.mul_right_eq_zero_iff_eq_zero u
+by cases hu with u hu; exact hu ▸ units.mul_right_eq_zero_iff_eq_zero u
 
 end semiring
 

src/analysis/asymptotics.lean

@@ -774,7 +774,7 @@ theorem is_O_with_self_const_mul (c : 𝕜) (hc : c ≠ 0) (f : α → 𝕜) (l
 
 theorem is_O_self_const_mul' {c : R} (hc : is_unit c) (f : α → R) (l : filter α) :
   is_O f (λ x, c * f x) l :=
-let ⟨u, hu⟩ := hc in hu.symm ▸ (is_O_with_self_const_mul' u f l).is_O
+let ⟨u, hu⟩ := hc in hu ▸ (is_O_with_self_const_mul' u f l).is_O
 
 theorem is_O_self_const_mul (c : 𝕜) (hc : c ≠ 0) (f : α → 𝕜) (l : filter α) :
   is_O f (λ x, c * f x) l :=

src/data/fintype/basic.lean

@@ -661,6 +661,25 @@ instance pfun_fintype (p : Prop) [decidable p] (α : p → Type*)
 if hp : p then fintype.of_equiv (α hp) ⟨λ a _, a, λ f, f hp, λ _, rfl, λ _, rfl⟩
           else ⟨singleton (λ h, (hp h).elim), by simp [hp, function.funext_iff]⟩
 
+lemma mem_image_univ_iff_mem_range
+  {α β : Type*} [fintype α] [decidable_eq β] {f : α → β} {b : β} :
+  b ∈ univ.image f ↔ b ∈ set.range f :=
+by simp
+
+lemma card_lt_card_of_injective_of_not_mem
+  {α β : Type*} [fintype α] [fintype β] (f : α → β) (h : function.injective f)
+  {b : β} (w : b ∉ set.range f) : fintype.card α < fintype.card β :=
+begin
+  classical,
+  calc
+    fintype.card α = (univ : finset α).card : rfl
+  ... = (image f univ).card : (card_image_of_injective univ h).symm
+  ... < (insert b (image f univ)).card :
+          card_lt_card (ssubset_insert (mt mem_image_univ_iff_mem_range.mp w))
+  ... ≤ (univ : finset β).card : card_le_of_subset (subset_univ _)
+  ... = fintype.card β : rfl
+end
+
 def quotient.fin_choice_aux {ι : Type*} [decidable_eq ι]
   {α : ι → Type*} [S : ∀ i, setoid (α i)] :
   ∀ (l : list ι), (∀ i ∈ l, quotient (S i)) → @quotient (Π i ∈ l, α i) (by apply_instance)

src/group_theory/group_action.lean

@@ -253,7 +253,7 @@ not_congr u.smul_eq_zero
 
 @[simp] theorem is_unit.smul_eq_zero {u : α} (hu : is_unit u) {x : β} :
   u • x = 0 ↔ x = 0 :=
-exists.elim hu $ λ u hu, hu.symm ▸ u.smul_eq_zero
+exists.elim hu $ λ u hu, hu ▸ u.smul_eq_zero
 
 variable (β)
 

src/group_theory/monoid_localization.lean

@@ -262,7 +262,7 @@ variables (f : localization_map S N)
 begin
   rw [f.to_map.map_mul, f.to_map.map_mul] at h,
   cases f.map_units c with u hu,
-  rw hu at h,
+  rw ←hu at h,
   exact (units.mul_right_inj u).1 h,
 end
 
@@ -380,7 +380,7 @@ by rw [mul_comm, mk'_mul_cancel_right]
   is_unit (j.comp f.to_map y) :=
 ⟨units.map j $ is_unit.lift_right (f.to_map.restrict S) f.map_units y,
   show j _ = j _, from congr_arg j $
-    (is_unit.coe_lift_right (f.to_map.restrict S) f.map_units _).symm⟩
+    (is_unit.coe_lift_right (f.to_map.restrict S) f.map_units _)⟩
 
 variables {g : M →* P}