FormalConjectures/Mathoverflow/507128.lean

GitHub source file

1 declarations, 1 contain sorry, 0 declared as axioms

Mathoverflow 507128

Reference: mathoverflow/507128 asked by user Junyan Xu

Imports (1)
  1. theorem Mathoverflow507128.exists_isFractionRing_self_ideal_ne_top_invertible sorry line 45 source

    depends on sorry what this means

    Statement uses: Exists, CommRing, IsFractionRing, Ideal, And, Ne, Top.top, Module.Invertible, Subtype, Membership.mem

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat

    21 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.