Main results

The main results that the formalization.yaml of FormalFrontier/quadratic-algebras lists under status.main_results at commit 16a5b4c5, each that the scan finds declared in the file the yaml gives, with its line. They are listed here, not made articles: in several Formal Frontier libraries this list is close to the whole API. The notes are the yaml's.

The scan does not find 1 of them; the library's page names it.

Declaration	Kind	Where
`QuadraticAlgebra.equivAdjoinRoot`	def	QuadraticAlgebras/AdjoinRoot.lean, line 116
`QuadraticAlgebra.exists_sq_eq_neg_discr_of_irreducible`	theorem	QuadraticAlgebras/RealClosedCoordinates.lean, line 71
`QuadraticAlgebra.equivOfDiscrSqNeg`	def	QuadraticAlgebras/RealClosedCoordinates.lean, line 96
`QuadraticAlgebra.adjoinRootEquivOfDiscrSqNeg`	def	QuadraticAlgebras/RealClosedCoordinates.lean, line 148
`IsRealClosed.irreducible_natDegree_le_two`	theorem	QuadraticAlgebras/RealClosedClosure.lean, line 315
`QuadraticAlgebra.adjoinRootEquivOfRoot`	def	QuadraticAlgebras/RealClosedAdjoinRoot.lean, line 52
`QuadraticAlgebra.adjoinRootEquivOfIrreducible`	def	QuadraticAlgebras/RealClosedAdjoinRoot.lean, line 122
`QuadraticAlgebra.realComplexEquiv`	def	QuadraticAlgebras/RealComplexAdjoinRoot.lean, line 47
`QuadraticAlgebra.adjoinRootComplexEquivOfRoot`	def	QuadraticAlgebras/RealComplexAdjoinRoot.lean, line 88
`QuadraticAlgebra.adjoinRootComplexEquivOfIrreducible`	def	QuadraticAlgebras/RealComplexAdjoinRoot.lean, line 142
`QuadraticAlgebra.fractionRingEquivBaseChange`	def	QuadraticAlgebras/FractionRing.lean, line 224
`IsFractionRing.isInteger_of_sq_mul_squarefree`	theorem	QuadraticAlgebras/Squarefree.lean, line 44
`QuadraticAlgebra.isIntegrallyClosed_iff_squarefree`	theorem	QuadraticAlgebras/IntegralClosureCriterion.lean, line 43
`QuadraticAlgebra.isIntegrallyClosed_int_of_squarefree_of_emod_four`	theorem	QuadraticAlgebras/IntegralClosureInt.lean, line 138
`MvPolynomial.irreducible_sumSMulXSq`	theorem	QuadraticAlgebras/Diagonal.lean, line 226
`MvPolynomial.squarefree_sumSMulXSq`	theorem	QuadraticAlgebras/Diagonal.lean, line 441
`QuadraticAlgebra.not_uniqueFactorizationMonoid_int_negFive`	theorem	QuadraticAlgebras/SqrtNegFive.lean, line 147
`QuadraticAlgebra.classNumber_sqrtNegFiveField`	theorem	QuadraticAlgebras/ClassNumberNegFive.lean, line 333

Quoted from the main results in formalization.yaml of FormalFrontier/quadratic-algebras at commit 16a5b4c5, Apache-2.0.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.