FLT/Mathlib/RingTheory/LocalRing/Defs.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Defs

Material destined for Mathlib.

Imports (3)
Imported by 2 files
  1. instance IsLocalRing.quot line 24 source

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

    Statement uses: CommRing, IsLocalRing, Ideal, Nontrivial, HasQuotient.Quotient

    Proof uses: IsLocalRing.of_surjective', Ideal.Quotient.mk, Ideal.Quotient.mk_surjective

    10 instances, coercions and auxiliary constants left out.

  2. instance IsLocalHom.quotient_mk line 26 source

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

    Statement uses: CommRing, IsLocalRing, Ideal, Nontrivial, HasQuotient.Quotient, IsLocalHom, RingHom, Algebra.algebraMap

    Proof uses: IsLocalHom.of_surjective, Ideal.Quotient.mk_surjective

    18 instances, coercions and auxiliary constants left out.