FLT/Mathlib/RingTheory/LocalRing/MaximalIdeal/Basic.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Basic

Material destined for Mathlib.

Imports (2)
Imported by 2 files
  1. theorem IsLocalRing.maximalIdeal_le line 19 source

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

    Statement uses: CommSemiring, IsLocalRing, Ideal, Ne, Top.top, LE.le, IsLocalRing.maximalIdeal, Ideal.IsMaximal

    Proof uses: Eq.rec, Eq, Ideal.IsMaximal.eq_of_le

    15 instances, coercions and auxiliary constants left out.