FLT/Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Pinned FLT blueprint introduction

1 declarations, 0 contain sorry, 0 declared as axioms

A group with two elements is Multiplicative (ZMod 2)

Material for Mathlib.GroupTheory.SpecificGroups.Cyclic.

Imports (2)
Imported by 2 files
  1. def mulEquivMultiplicativeZModTwo Documented declaration: mulEquivMultiplicativeZModTwo line 23 source

    Source documentation

    A group G with exactly two elements — the identity 1 and a distinguished element g ≠ 1, every element being equal to one of the two — is isomorphic to Multiplicative (ZMod 2), via the isomorphism sending g to Multiplicative.ofAdd 1. The generator g and the exhaustion key are taken as explicit data (rather than a bare Nat.card G = 2) so the isomorphism is computable.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Group, DecidableEq, Ne, OfNat.ofNat, Or, Eq, MulEquiv, Multiplicative, ZMod, Nat

    Proof uses: HMul.hMul, Equiv, Multiplicative.ofAdd, MulEquiv.mk, Equiv.mk, ite

    54 instances, coercions and auxiliary constants left out.

    Tactic trace: 10 steps

    Open to load the checked before-and-after goal states.

    def mulEquivMultiplicativeZModTwo {G : Type*} [Group G] [DecidableEq G] (g : G) (hg : g ≠ 1)
    (key : ∀ x : G, x = 1 ∨ x = g) : G ≃* Multiplicative (ZMod 2) :=
…