FLT/Mathlib/GroupTheory/Index.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

TODO

Imports (7)
Imported by 3 files
  1. theorem Subgroup.index_op line 33 source

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

    Statement uses: Group, Subgroup, Eq, Nat, Subgroup.index, MulOpposite, Subgroup.op

    Proof uses: Trans.simple, Subgroup.comap, MulEquiv.toMonoidHom, MulEquiv.symm, MulEquiv.inv', Eq.rec, Eq.refl, Subgroup.ext, of_eq_true, Iff, Membership.mem, Eq.trans, MulOpposite.unop, True, congr, congrArg, MulEquiv, MonoidHom, Inv.inv, congrFun and 5 more

    28 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

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

  2. instance (instance at line 40) line 40 source