Beta

Finite group action

3mhimmel
Description
Loading description...
Algorithms
View
AllIssues2QuestionsSuggestionsShow Resolved
  • Please sign in or sign up to leave a comment.
  • donaldsebleung Avatar

    This Kata is not compatible with Lean v3.18.4 as of 16/08/2020 and needs to be upgraded.

  • kckennylau Avatar

    In Preloaded.lean you have:

    def SUBMISSION : Prop :=
∀ {G : Type} [group G] [fintype G] (hG65 : fintype.card G = 65)
  {M : Type} [fintype M] (hM27 : fintype.card M = 27) [mul_action G M] :
  ∃ m : M, ∀ g : G, g • m = m

    which does not match with the following in the initial solution:

    theorem has_fixed_point {G : Type} [fintype G] [group G] (hG65 : fintype.card G = 65)
  {M : Type} [fintype M] (hM27 : fintype.card M = 27) [mul_action G M] :
  ∃ m : M, ∀ g : G, g • m = m := sorry

    (the order of [fintype G] and [group G] are different)