PFR/Mathlib/Algebra/Group/Action/Pointwise/Set/Basic.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)
Imported by 2 files
  1. lemma Set.singleton_mul' line 15 source

    standard axioms: Quot.sound, propext what this means

    Statement uses: Mul, Set, Eq, HMul.hMul, Singleton.singleton, HSMul.hSMul

    Proof uses: Set.singleton_mul

    6 instances, coercions and auxiliary constants left out.

  2. lemma Set.mul_singleton' line 18 source

    standard axioms: Quot.sound, propext what this means

    Statement uses: Mul, Set, Eq, HMul.hMul, Singleton.singleton, HSMul.hSMul, MulOpposite, MulOpposite.op

    Proof uses: Set.mul_singleton

    6 instances, coercions and auxiliary constants left out.