Incompatible notations

Stream: mathlib4

[Patrick Massot]

In the next example, uncommenting the first line breaks everything.

-- import Mathlib
import Mathlib.Geometry.Manifold.ContMDiffMap

open scoped Manifold

variable {E : Type _} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type _} [TopologicalSpace H]
  (I : ModelWithCorners ℝ E H) (M : Type _) [TopologicalSpace M] [ChartedSpace H M]
  [SmoothManifoldWithCorners I M] {E' : Type _} [NormedAddCommGroup E'] [NormedSpace ℝ E']
  {H' : Type _} [TopologicalSpace H'] (I' : ModelWithCorners ℝ E' H') (M' : Type _)
  [TopologicalSpace M'] [ChartedSpace H' M']
  (n : ℕ)

#check C^n⟮I, M; I', M'⟯

[Patrick Massot]

import Mathlib.FieldTheory.Adjoin is enough :angry:

[Patrick Massot]

Note the open scoped Manifold says which notation is a good citizen.

[Eric Wieser]

In case you haven't already found it, the offending notation is here

[Patrick Massot]

I know, thanks.

[Patrick Massot]

The funny thing is that this notation also conflict with a third notation (that is already scoped) in elliptic curves (so this is not a story of algebra fighting geometry).

[Patrick Massot]

Fixed at #7938

[Eric Rodriguez]

Yeah, I ran into this whilst trying to fix an unrelated breakage before - thanks for fixing it!