Documentation Verification Report

Bivariate

📁 Source: Mathlib/RingTheory/Adjoin/Polynomial/Bivariate.lean

Statistics

Metric	Count
Definitions `algEquivAdjoin`	1
Theorems `adjoin_singleton`, `algEquivAdjoin_apply`, `algEquivAdjoin_swap_eq_aeval`, `aeval_aeval_eq_aeval_algEquivAdjoin`	4
Total	5

IsAlgebraic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adjoin_singleton` 📖	mathematical	`Transcendental` `CommRing.toRing` `IsAlgebraic` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set` `Set.instSingletonSet` `Algebra.instCommRingAdjoinSingleton` `Subalgebra.toAlgebra` `Ring.toSemiring`	`IsAlgebraic` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set` `Set.instSingletonSet` `Algebra.instCommRingAdjoinSingleton` `CommRing.toRing` `Subalgebra.toAlgebra` `Ring.toSemiring` `Algebra.id` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap`	—	`map_ne_zero_iff` `AlgEquiv.injective` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `Algebra.self_mem_adjoin_singleton` `Polynomial.Bivariate.Transcendental.algEquivAdjoin_swap_eq_aeval` `Polynomial.Bivariate.aeval_aeval_eq_aeval_algEquivAdjoin` `AlgEquiv.apply_symm_apply`

Polynomial.Bivariate

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`aeval_aeval_eq_aeval_algEquivAdjoin` 📖	mathematical	`Transcendental` `CommRing.toRing`	`DFunLike.coe` `AlgHom` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set` `Set.instSingletonSet` `Polynomial` `Algebra.instCommSemiringAdjoinSingleton` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `Subalgebra.toAlgebra` `AlgHom.funLike` `Polynomial.aeval` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap` `Polynomial.commSemiring` `Subalgebra.toSemiring` `Polynomial.algebra` `Subalgebra.algebra` `Polynomial.C` `Algebra.self_mem_adjoin_singleton` `Ring.toSemiring` `CommRing.toRing` `AlgEquiv` `AlgEquiv.instFunLike` `Transcendental.algEquivAdjoin`	—	`Polynomial.induction_on'` `Algebra.self_mem_adjoin_singleton` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `Polynomial.aeval_monomial` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `Polynomial.aeval_map_algebraMap` `IsScalarTower.subalgebra'` `IsScalarTower.right` `Polynomial.aeval_algebraMap_apply` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `Polynomial.aeval_C` `Polynomial.map_monomial` `Polynomial.coe_aeval_mk_apply`

Polynomial.Bivariate.Transcendental

Definitions

Name	Category	Theorems
`algEquivAdjoin` 📖	CompOp	3 math math: `algEquivAdjoin_apply`, `Polynomial.Bivariate.aeval_aeval_eq_aeval_algEquivAdjoin`, `algEquivAdjoin_swap_eq_aeval`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algEquivAdjoin_apply` 📖	mathematical	`Transcendental`	`DFunLike.coe` `AlgEquiv` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.semiring` `Subalgebra` `Ring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set` `Set.instSingletonSet` `Subalgebra.toSemiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `Subalgebra.algebra` `AlgEquiv.instFunLike` `algEquivAdjoin` `AlgHom` `AlgHom.funLike` `Polynomial.mapAlgHom` `Polynomial.aeval` `Algebra.self_mem_adjoin_singleton`	—	—
`algEquivAdjoin_swap_eq_aeval` 📖	mathematical	`Transcendental`	`DFunLike.coe` `AlgEquiv` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.semiring` `Subalgebra` `Ring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set` `Set.instSingletonSet` `Subalgebra.toSemiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `Subalgebra.algebra` `AlgEquiv.instFunLike` `algEquivAdjoin` `Polynomial.Bivariate.swap` `AlgHom` `Polynomial.commSemiring` `Polynomial.algebra` `AlgHom.funLike` `Polynomial.aeval` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `Polynomial.C` `Algebra.self_mem_adjoin_singleton`	—	`AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Algebra.self_mem_adjoin_singleton` `Polynomial.Bivariate.aveal_eq_map_swap`

---

← Back to Index