FLT/Mathlib/Topology/Algebra/RestrictedProduct/Algebra.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Lemmas about restricted products of algebras

Imports (2)
Imported by 2 files
  1. instance RestrictedProduct.piAlgebra line 21 source

    standard axioms: Quot.sound, propext what this means

    Statement uses: CommRing, SetLike, SubringClass, Filter, Algebra, Subtype, Membership.mem, RestrictedProduct, Subring, Subring.ofClass

    Proof uses: Algebra.compHom, RestrictedProduct.structureMapRingHom

    27 instances, coercions and auxiliary constants left out.

  2. lemma RestrictedProduct.piSmul_apply line 26 source

    standard axioms: Quot.sound, propext what this means

    Statement uses: CommRing, SetLike, SubringClass, Filter, Subtype, Membership.mem, RestrictedProduct, Subring, Subring.ofClass, Eq, HSMul.hSMul

    Proof uses: rfl

    36 instances, coercions and auxiliary constants left out.

  3. lemma RestrictedProduct.algebraMap_pi_apply line 30 source

    standard axioms: Quot.sound, propext what this means

    Statement uses: CommRing, SetLike, SubringClass, Filter, Subtype, Membership.mem, Eq, RestrictedProduct, Subring, Subring.ofClass, RingHom, Algebra.algebraMap

    Proof uses: rfl

    35 instances, coercions and auxiliary constants left out.