Documentation Verification Report

Laurent

📁 Source: Mathlib/FieldTheory/Laurent.lean

Statistics

Metric	Count
Definitions `laurent`, `laurentAux`	2
Theorems `laurentAux_algebraMap`, `laurentAux_div`, `laurentAux_ofFractionRing_mk`, `laurent_C`, `laurent_X`, `laurent_algebraMap`, `laurent_at_zero`, `laurent_div`, `laurent_injective`, `laurent_laurent`, `taylor_mem_nonZeroDivisors`	11
Total	13

RatFunc

Definitions

Name	Category	Theorems
`laurent` 📖	CompOp	7 math math: `laurent_injective`, `laurent_X`, `laurent_algebraMap`, `laurent_div`, `laurent_at_zero`, `laurent_laurent`, `laurent_C`
`laurentAux` 📖	CompOp	3 math math: `laurentAux_div`, `laurentAux_algebraMap`, `laurentAux_ofFractionRing_mk`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`laurentAux_algebraMap` 📖	mathematical	—	`DFunLike.coe` `RingHom` `RatFunc` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `RingHom.instFunLike` `laurentAux` `Polynomial` `Polynomial.commSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instField` `algebraMap` `instAlgebraOfPolynomial` `Algebra.id` `LinearMap` `RingHom.id` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Polynomial.semiring` `Polynomial.module` `Semiring.toModule` `LinearMap.instFunLike` `Polynomial.taylor`	—	`mk_one` `mk_eq_div` `laurentAux_div` `Polynomial.taylor_one` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`laurentAux_div` 📖	mathematical	—	`DFunLike.coe` `RingHom` `RatFunc` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `RingHom.instFunLike` `laurentAux` `instDiv` `Polynomial` `Polynomial.commSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instField` `algebraMap` `instAlgebraOfPolynomial` `Algebra.id` `LinearMap` `RingHom.id` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Polynomial.semiring` `Polynomial.module` `Semiring.toModule` `LinearMap.instFunLike` `Polynomial.taylor`	—	`map_apply_div` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `taylor_mem_nonZeroDivisors`
`laurentAux_ofFractionRing_mk` 📖	mathematical	—	`DFunLike.coe` `RingHom` `RatFunc` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `RingHom.instFunLike` `laurentAux` `ofFractionRing` `Polynomial` `CommRing.toCommMonoid` `Polynomial.commRing` `nonZeroDivisors` `Semiring.toMonoidWithZero` `LinearMap` `RingHom.id` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Polynomial.semiring` `Polynomial.module` `Semiring.toModule` `LinearMap.instFunLike` `Polynomial.taylor` `Submonoid` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `SetLike.instMembership` `Submonoid.instSetLike` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `taylor_mem_nonZeroDivisors` `Subtype.prop`	—	`MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `taylor_mem_nonZeroDivisors`
`laurent_C` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `RatFunc` `CommRing.toCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instField` `instAlgebraOfPolynomial` `Polynomial.algebraOfAlgebra` `CommSemiring.toSemiring` `Algebra.id` `AlgHom.funLike` `laurent` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `C`	—	`algebraMap_C` `laurent_algebraMap` `Polynomial.taylor_C`
`laurent_X` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `RatFunc` `CommRing.toCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instField` `instAlgebraOfPolynomial` `Polynomial.algebraOfAlgebra` `CommSemiring.toSemiring` `Algebra.id` `AlgHom.funLike` `laurent` `X` `instAdd` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `C`	—	`algebraMap_X` `laurent_algebraMap` `Polynomial.taylor_X` `map_add` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `algebraMap_C`
`laurent_algebraMap` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `RatFunc` `CommRing.toCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instField` `instAlgebraOfPolynomial` `Polynomial.algebraOfAlgebra` `CommSemiring.toSemiring` `Algebra.id` `AlgHom.funLike` `laurent` `RingHom` `Polynomial` `Semiring.toNonAssocSemiring` `Polynomial.commSemiring` `RingHom.instFunLike` `algebraMap` `LinearMap` `RingHom.id` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Polynomial.semiring` `Polynomial.module` `Semiring.toModule` `LinearMap.instFunLike` `Polynomial.taylor`	—	`laurentAux_algebraMap`
`laurent_at_zero` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `RatFunc` `CommRing.toCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instField` `instAlgebraOfPolynomial` `Polynomial.algebraOfAlgebra` `CommSemiring.toSemiring` `Algebra.id` `AlgHom.funLike` `laurent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`induction_on` `map_div₀` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `laurent_algebraMap` `Polynomial.taylor_zero'`
`laurent_div` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `RatFunc` `CommRing.toCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instField` `instAlgebraOfPolynomial` `Polynomial.algebraOfAlgebra` `CommSemiring.toSemiring` `Algebra.id` `AlgHom.funLike` `laurent` `instDiv` `RingHom` `Polynomial` `Semiring.toNonAssocSemiring` `Polynomial.commSemiring` `RingHom.instFunLike` `algebraMap` `LinearMap` `RingHom.id` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Polynomial.semiring` `Polynomial.module` `Semiring.toModule` `LinearMap.instFunLike` `Polynomial.taylor`	—	`laurentAux_div`
`laurent_injective` 📖	mathematical	—	`RatFunc` `DFunLike.coe` `AlgHom` `CommRing.toCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instField` `instAlgebraOfPolynomial` `Polynomial.algebraOfAlgebra` `CommSemiring.toSemiring` `Algebra.id` `AlgHom.funLike` `laurent`	—	`laurent_laurent` `neg_add_cancel` `laurent_at_zero`
`laurent_laurent` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `RatFunc` `CommRing.toCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instField` `instAlgebraOfPolynomial` `Polynomial.algebraOfAlgebra` `CommSemiring.toSemiring` `Algebra.id` `AlgHom.funLike` `laurent` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`induction_on` `laurent_div` `Polynomial.taylor_taylor`
`taylor_mem_nonZeroDivisors` 📖	mathematical	`Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `Polynomial.semiring` `SetLike.instMembership` `Submonoid.instSetLike` `nonZeroDivisors`	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Polynomial.module` `Semiring.toModule` `LinearMap.instFunLike` `Polynomial.taylor`	—	`mem_nonZeroDivisors_iff_right` `sub_self` `Polynomial.taylor_zero'` `LinearMap.map_eq_zero_iff` `Polynomial.taylor_injective` `mul_right_mem_nonZeroDivisors_eq_zero_iff` `Polynomial.taylor_mul` `Polynomial.taylor_taylor` `sub_eq_add_neg`

---

← Back to Index