FormalConjecturesForMathlib/Algebra/QuadraticAlgebra/Instances.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Imports (2)
Imported by 2 files
  1. instance QuadraticAlgebra.(instance at line 27) line 27 source
  2. lemma QuadraticAlgebra.algebraMap_omega line 33 source

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

    Statement uses: CommSemiring, CommRing, Algebra, Eq, QuadraticAlgebra, RingHom, Algebra.algebraMap, QuadraticAlgebra.omega

    Proof uses: Eq.mpr, HMul.hMul, HAdd.hAdd, HSMul.hSMul, OfNat.ofNat, Equiv, AlgHom, Subtype, Equiv.symm, QuadraticAlgebra.lift, Subtype.mk, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, of_eq_true, Eq.trans, True, congrArg and 9 more

    66 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  3. instance QuadraticAlgebra.(instance at line 38) line 38 source
  4. lemma QuadraticAlgebra.algebraMap_omega' line 42 source

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

    Statement uses: CommRing, Int, Eq, QuadraticAlgebra, RingHom, Algebra.algebraMap, QuadraticAlgebra.omega

    Proof uses: QuadraticAlgebra.algebraMap_omega

    21 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  5. instance QuadraticAlgebra.(instance at line 46) line 46 source
  6. lemma QuadraticAlgebra.algebraMap_omega'' line 50 source

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

    Statement uses: CommRing, Int, Eq, QuadraticAlgebra, OfNat.ofNat, RingHom, Algebra.algebraMap, QuadraticAlgebra.omega

    Proof uses: Eq.mpr, HMul.hMul, HAdd.hAdd, HSMul.hSMul, Equiv, AlgHom, Subtype, Equiv.symm, QuadraticAlgebra.lift, Subtype.mk, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, of_eq_true, Eq.trans, True, congrArg, QuadraticAlgebra.re and 8 more

    75 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  7. instance QuadraticAlgebra.fact_field line 57 source

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

    Statement uses: Int, Fact, Squarefree, Ne, OfNat.ofNat, Rat, HPow.hPow, Nat, HAdd.hAdd, HMul.hMul

    Proof uses: Fact.mk, Eq, IsSquare, False, Iff.mp, Rat.isSquare_intCast_iff, Exists.intro

    32 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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