FormalConjecturesForMathlib/Algebra/Group/Action/Pointwise/Set/Basic.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)
Imported by 2 files
  1. lemma Set.mul_mem_smul_set line 28 source

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

    Statement uses: Monoid, Set, IsLeftCancelMul, Iff, Membership.mem, HSMul.hSMul, HMul.hMul

    Proof uses: Function.Injective.mem_set_image, mul_right_injective

    12 instances, coercions and auxiliary constants left out.