Commit 2020-09-14 08:03 1c2ddbcf

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

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

Estimated changes

Created src/algebra/big_operators/finsupp.lean

added theorem finset.sum_apply'

added theorem finsupp.sum_apply'

added theorem finsupp.sum_sum_index'

Modified src/algebra/group_ring_action.lean

added theorem eq_of_smul_eq_smul

added theorem injective_to_semiring_hom

Modified src/data/set/function.lean

added theorem set.inj_on_insert

Modified src/field_theory/fixed.lean

added theorem cardinal_mk_alg_hom

added theorem findim_alg_hom

modified theorem fixed_points.coe_algebra_map

added theorem fixed_points.coe_to_alg_hom

added theorem fixed_points.dim_le_card

added theorem fixed_points.findim_eq_card

added theorem fixed_points.findim_le_card

modified theorem fixed_points.is_integral

added theorem fixed_points.linear_independent_smul_of_linear_independent

modified theorem fixed_points.minpoly.eval₂

modified theorem fixed_points.minpoly.irreducible

modified theorem fixed_points.minpoly.irreducible_aux

modified theorem fixed_points.minpoly.minimal_polynomial

modified theorem fixed_points.minpoly.monic

modified theorem fixed_points.minpoly.ne_one

added theorem fixed_points.minpoly.of_eval₂

modified def fixed_points.minpoly

deleted theorem fixed_points.of_eval₂

modified theorem fixed_points.smul

modified theorem fixed_points.smul_polynomial

added def fixed_points.to_alg_hom

added theorem fixed_points.to_alg_hom_apply

added theorem linear_independent_to_linear_map

Modified src/field_theory/tower.lean

added theorem finite_dimensional.findim_linear_map'

added theorem finite_dimensional.findim_linear_map

added theorem finite_dimensional.right

Modified src/group_theory/group_action.lean

added def mul_action.to_fun

added theorem mul_action.to_fun_apply

Modified src/linear_algebra/basis.lean

added theorem linear_independent.image'

added theorem linear_independent_equiv'

added theorem linear_independent_equiv

added theorem linear_independent_image

added theorem linear_independent_insert'

added theorem linear_independent_insert

added theorem linear_independent_of_comp

Modified src/linear_algebra/dimension.lean

added theorem dim_le

added theorem is_basis.mk_eq_dim''

added theorem {u₁}

Modified src/linear_algebra/finsupp.lean

added theorem finsupp.total_apply_of_mem_supported

Modified src/ring_theory/algebra.lean

added def linear_map.lto_fun

Modified src/ring_theory/algebra_tower.lean

Modified src/set_theory/cardinal.lean

added theorem cardinal.card_le_of