FLT/Mathlib/Data/Fin/Basic.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Basic

Material destined for Mathlib.

Imports (1)
Imported by 1 file
  1. theorem Fin.pairwise_forall_two line 18 source

    standard axioms: Quot.sound, propext what this means

    Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, Pairwise, Nat.succ, Function.onFun, Matrix.vecCons, Fin.last, Matrix.vecEmpty

    Proof uses: Pairwise.comp_of_injective, of_eq_true, Eq, Eq.trans, And, True, forall_congr, congrArg, implies_congr, Matrix.cons_val_fin_one, Eq.refl, congr, eq_self, False, and_false, and_self, congrFun'

    20 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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