Commit 2025-09-28 12:07 4eca3e81

View on Github →

feat(InfinitePlace/Embeddings): remove dependency of IsMixed/IsUnmixed on Extension. (#29945)

  • Remove the unnecessary dependency of ComplexEmbedding.IsUnmixed on the subtype ComplexEmbedding.Extension, which makes it easier to use as it does not require the construction of a term of ComplexEmbedding.Extension. This also aligns it more closely with InfinitePlace.IsUnramified, of which it is intended to be an analogue.
  • Ditto for ComplexEmbedding.IsMixed.
  • The definition of IsUnmixed is now given in simp-normal form.

Estimated changes