laurent): Laurent polynomials are a localization of polynomials (#14489)

Commit

3 years ago

feat(data/polynomial/laurent): Laurent polynomials are a localization of polynomials (#14489) This PR proves the lemma `is_localization (submonoid.closure ({X} : set R[X])) R[T;T⁻¹]`.

Author

adomani

Parents

4a3b22e5

mathlib3 579d6f9e - feat(data/polynomial/laurent): Laurent polynomials are a localization of polynomials (#14489)

mathlib3
579d6f9e - feat(data/polynomial/laurent): Laurent polynomials are a localization of polynomials (#14489)