PFR/Mathlib/Data/ZMod/Basic.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)
Imported by 3 files
  1. lemma Set.sub_eq_add line 13 source

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

    Statement uses: AddCommGroup, Module, ZMod, OfNat.ofNat, Nat, Set, Eq, HSub.hSub, HAdd.hAdd

    Proof uses: of_eq_true, Set.image2, Eq.trans, True, congrFun', congrArg, Set.image2_congr, Membership.mem, ZModModule.sub_eq_add, eq_self

    30 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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