FLT/Mathlib/RingTheory/Ideal/Quotient/Basic.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Basic

Material destined for Mathlib.

Imports (1)
Imported by 2 files
  1. theorem Ideal.Quotient.out_sub line 20 source

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

    Statement uses: Ring, Ideal, Ideal.IsTwoSided, Membership.mem, HSub.hSub, Quotient.out, Submodule.quotientRel, RingHom, HasQuotient.Quotient, Ideal.Quotient.mk

    Proof uses: Eq.mpr, Eq, id, congrArg, Eq.symm, propext, Ideal.Quotient.eq, Ideal.Quotient.mk_out, Eq.refl

    32 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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