feat(field_theory/fixed): dimension over fixed field is order of group (#4125)

```lean
theorem dim_fixed_points (G : Type u) (F : Type v) [group G] [field F]
  [fintype G] [faithful_mul_semiring_action G F] :
  findim (fixed_points G F) F = fintype.card G
````

Author: kckennylau

src/algebra/big_operators/finsupp.lean

@@ -0,0 +1,40 @@
+/-
+Copyright (c) 2020 Kenny Lau. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kenny Lau
+-/
+
+import algebra.big_operators.pi
+import data.finsupp
+
+/-!
+# Big operators for finsupps
+
+This file contains theorems relevant to big operators in finitely supported functions.
+-/
+
+universes u v w u₁ v₁ w₁
+
+open_locale big_operators
+
+variables {α : Type u} {ι : Type v} {β : Type w} [add_comm_monoid β]
+variables {s : finset α} {f : α → (ι →₀ β)} (i : ι)
+
+theorem finset.sum_apply' : (∑ k in s, f k) i = ∑ k in s, f k i :=
+(s.sum_hom $ finsupp.eval_add_hom i).symm
+
+variables {γ : Type u₁} {δ : Type v₁} [add_comm_monoid δ]
+variables (g : ι →₀ β) (k : ι → β → γ → δ) (x : γ)
+
+theorem finsupp.sum_apply' : g.sum k x = g.sum (λ i b, k i b x) :=
+finset.sum_apply _ _ _
+
+variables {ε : Type w₁} [add_comm_monoid ε]
+variables {t : ι → β → ε} (h0 : ∀ i, t i 0 = 0) (h1 : ∀ i x y, t i (x + y) = t i x + t i y)
+include h0 h1
+
+open_locale classical
+
+theorem finsupp.sum_sum_index' : (∑ x in s, f x).sum t = ∑ x in s, (f x).sum t :=
+finset.induction_on s rfl $ λ a s has ih,
+by simp_rw [finset.sum_insert has, finsupp.sum_add_index h0 h1, ih]

src/algebra/group_ring_action.lean

@@ -38,6 +38,11 @@ class mul_semiring_action (M : Type u) [monoid M] (R : Type v) [semiring R]
 
 export mul_semiring_action (smul_one)
 
+/-- Typeclass for faithful multiplicative actions by monoids on semirings. -/
+class faithful_mul_semiring_action (M : Type u) [monoid M] (R : Type v) [semiring R]
+  extends mul_semiring_action M R :=
+(eq_of_smul_eq_smul' : ∀ {m₁ m₂ : M}, (∀ r : R, m₁ • r = m₂ • r) → m₁ = m₂)
+
 section semiring
 
 variables (M G : Type u) [monoid M] [group G]
@@ -48,6 +53,11 @@ lemma smul_mul' [mul_semiring_action M R] (g : M) (x y : R) :
   g • (x * y) = (g • x) * (g • y) :=
 mul_semiring_action.smul_mul g x y
 
+variables {M} (R)
+theorem eq_of_smul_eq_smul [faithful_mul_semiring_action M R] {m₁ m₂ : M} :
+  (∀ r : R, m₁ • r = m₂ • r) → m₁ = m₂ :=
+faithful_mul_semiring_action.eq_of_smul_eq_smul'
+
 variables (M R)
 
 /-- Each element of the monoid defines a additive monoid homomorphism. -/
@@ -73,6 +83,10 @@ def mul_semiring_action.to_semiring_hom [mul_semiring_action M R] (x : M) : R 
   map_mul' := smul_mul' x,
   .. distrib_mul_action.to_add_monoid_hom M R x }
 
+theorem injective_to_semiring_hom [faithful_mul_semiring_action M R] :
+  function.injective (mul_semiring_action.to_semiring_hom M R) :=
+λ m₁ m₂ h, eq_of_smul_eq_smul R $ λ r, ring_hom.ext_iff.1 h r
+
 /-- Each element of the group defines a semiring isomorphism. -/
 def mul_semiring_action.to_semiring_equiv [mul_semiring_action G R] (x : G) : R ≃+* R :=
 { .. distrib_mul_action.to_add_equiv G R x,
@@ -110,9 +124,7 @@ end simp_lemmas
 
 namespace polynomial
 
-variables [mul_semiring_action M S]
-
-noncomputable instance : mul_semiring_action M (polynomial S) :=
+noncomputable instance [mul_semiring_action M S] : mul_semiring_action M (polynomial S) :=
 { smul := λ m, map $ mul_semiring_action.to_semiring_hom M S m,
   one_smul := λ p, by { ext n, erw coeff_map, exact one_smul M (p.coeff n) },
   mul_smul := λ m n p, by { ext i,
@@ -123,6 +135,17 @@ noncomputable instance : mul_semiring_action M (polynomial S) :=
   smul_one := λ m, map_one (mul_semiring_action.to_semiring_hom M S m),
   smul_mul := λ m p q, map_mul (mul_semiring_action.to_semiring_hom M S m), }
 
+noncomputable instance [faithful_mul_semiring_action M S] :
+  faithful_mul_semiring_action M (polynomial S) :=
+{ eq_of_smul_eq_smul' := λ m₁ m₂ h, eq_of_smul_eq_smul S $ λ s, C_inj.1 $
+    calc  C (m₁ • s)
+        = m₁ • C s : (map_C $ mul_semiring_action.to_semiring_hom M S m₁).symm
+    ... = m₂ • C s : h (C s)
+    ... = C (m₂ • s) : map_C _,
+  .. polynomial.mul_semiring_action M S }
+
+variables [mul_semiring_action M S]
+
 @[simp] lemma coeff_smul' (m : M) (p : polynomial S) (n : ℕ) :
   (m • p).coeff n = m • p.coeff n :=
 coeff_map _ _

src/data/set/function.lean

@@ -187,6 +187,18 @@ theorem eq_on.inj_on_iff (H : eq_on f₁ f₂ s) : inj_on f₁ s ↔ inj_on f₂
 theorem inj_on.mono (h : s₁ ⊆ s₂) (ht : inj_on f s₂) : inj_on f s₁ :=
 λ x hx y hy H, ht (h hx) (h hy) H
 
+theorem inj_on_insert {f : α → β} {s : set α} {a : α} (has : a ∉ s) :
+  set.inj_on f (insert a s) ↔ set.inj_on f s ∧ f a ∉ f '' s :=
+⟨λ hf, ⟨hf.mono $ subset_insert a s,
+  λ ⟨x, hxs, hx⟩, has $ mem_of_eq_of_mem (hf (or.inl rfl) (or.inr hxs) hx.symm) hxs⟩,
+λ ⟨h1, h2⟩ x hx y hy hfxy, or.cases_on hx
+  (λ hxa : x = a, or.cases_on hy
+    (λ hya : y = a, hxa.trans hya.symm)
+    (λ hys : y ∈ s, h2.elim ⟨y, hys, hxa ▸ hfxy.symm⟩))
+  (λ hxs : x ∈ s, or.cases_on hy
+    (λ hya : y = a, h2.elim ⟨x, hxs, hya ▸ hfxy⟩)
+    (λ hys : y ∈ s, h1 hxs hys hfxy))⟩
+
 lemma injective_iff_inj_on_univ : injective f ↔ inj_on f univ :=
 ⟨λ h x hx y hy hxy, h hxy, λ h _ _ heq, h trivial trivial heq⟩