OAI/RingTheory/DirectFiniteness/PrescribedOutputs.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.KaplanskyCounterexample.Prescription.Output.G line 13

    Source documentation

    The group in the literal prescription: the coordinate gluing, its multiple HNN extension and the finite permutation/character block.

    abbrev G := ChosenCriterion.Group (m := Slots) ell Inc assignment nonempty_Inc girth_Inc v0 form

    Mentions: OAI.KaplanskyCounterexample.ChosenCriterion.Group, OAI.KaplanskyCounterexample.Prescription.Output.Slots, OAI.KaplanskyCounterexample.Prescription.Output.ell, OAI.KaplanskyCounterexample.Prescription.Output.Inc, OAI.KaplanskyCounterexample.Prescription.Output.assignment, OAI.KaplanskyCounterexample.Prescription.Output.nonempty_Inc, OAI.KaplanskyCounterexample.Prescription.Output.girth_Inc, OAI.KaplanskyCounterexample.Prescription.Output.v0, OAI.KaplanskyCounterexample.Prescription.Output.form

  2. def OAI.KaplanskyCounterexample.Prescription.Output.a line 15
  3. def OAI.KaplanskyCounterexample.Prescription.Output.b line 19
  4. theorem OAI.KaplanskyCounterexample.Prescription.Output.prescribed_products line 25

    Source documentation

    The two product assertions are for the specified first successful data and specified sums, not merely for some field, some group or some pair of inverses.

    theorem prescribed_products : a*b=1 ∧ b*a≠1 :=
…

    Mentions: OAI.KaplanskyCounterexample.Prescription.Output.a, OAI.KaplanskyCounterexample.Prescription.Output.b

  5. instance OAI.KaplanskyCounterexample.Prescription.Output.G_fg line 30
  6. def OAI.KaplanskyCounterexample.Prescription.Output.N_shortEquiv line 32
  7. lemma OAI.KaplanskyCounterexample.Prescription.Output.N_shortRelators_finite line 38
  8. theorem OAI.KaplanskyCounterexample.Prescription.Output.prescribed_main line 43

    Source documentation

    The literal prescription supplies the main existential witnesses.

    theorem prescribed_main :
    ∃ (K : Type) (_ : Field K) (_ : Fintype K) (_ : CharP K 2),
      ∃ (G : Type) (_ : Group G) (_ : Group.FG G),
        ∃ a b : MonoidAlgebra K G, a*b=1 ∧ b*a≠1 :=
…

    Mentions: OAI.KaplanskyCounterexample.Prescription.K, OAI.KaplanskyCounterexample.Prescription.Output.G, OAI.KaplanskyCounterexample.Prescription.Output.a, OAI.KaplanskyCounterexample.Prescription.Output.b