PFR/Mathlib/Order/Interval/Finset/Fin.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)
Imported by 2 files
  1. lemma Fin.Iio_succ_eq_Iic_castSucc line 11 source

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

    Statement uses: Nat, Fin, Eq, Finset, HAdd.hAdd, OfNat.ofNat, Finset.Iio, Fin.succ, Finset.Iic, Fin.castSucc

    Proof uses: rfl

    12 instances, coercions and auxiliary constants left out.