Module

LaurentPolynomial_isUnit_iff_exists_C_mul_T.lean

Nyll.AlgebraicCurves.Foundations.Polynomial.LaurentPolynomial_isUnit_iff_exists_C_mul_T

1 declaration indexed from sourceView source ↗

Module documentation

Laurent Polynomial is Unit iff exists C mul T

Imports2

Mathlib.Algebra.Polynomial.Laurent
Mathlib.Algebra.Polynomial.RingDivision

Imported by1

Nyll.AlgebraicCurves.Foundations.Polynomial.All

theorem

isUnit_iff_exists_C_mul_T

L28 ↗

LaurentPolynomial.isUnit_iff_exists_C_mul_T

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs.LaurentPolynomial_isUnit_iff_exists_C_mul_T
open LaurentPolynomial
universe u

Lean source · statement

theorem _root_.LaurentPolynomial.isUnit_iff_exists_C_mul_T
    {R : Type u} [CommRing R] [IsDomain R] (f : R[T;T⁻¹]) :
    IsUnit f ↔ ∃ (c : Rˣ) (n : ℤ), f = C (c : R) * T n

Module documentation

Laurent Polynomial is Unit iff exists C mul T

Declarations

isUnit_iff_exists_C_mul_T