FormalConjecturesForMathlib/Logic/Equiv/Fin/Rotate.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)
Imported by 2 files
  1. theorem lt_finRotate_of_ne_last line 24 source

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

    Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, Ne, Fin.last, LT.lt, Equiv.Perm, finRotate

    Proof uses: Eq.mpr, id, Eq, congrArg, propext, Fin.lt_def, Nat.succ, coe_finRotate_of_ne_last, LE.le, Nat.lt_add_one_iff, le_refl

    18 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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