Main.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.ComplexCancellation.nonpolynomiality line 10
Source documentation
The hypersurface algebra is not a polynomial algebra over ℂ.
```
theorem nonpolynomiality : ¬ Nonempty (A ≃ₐ[ℂ] MvPolynomial (Fin 4) ℂ) := by
…
```
Mentions: OAI.ComplexCancellation.A
theorem OAI.ComplexCancellation.main line 32
Source documentation
A four-dimensional complex domain with polynomial cylinder, but not itself polynomial.
Distinct definitions of this name: ComparatorChallenges/ComplexCancellation.lean:25 (same statement text; different proof or body). Qualify references as OAI.ComplexCancellation.main@path.
```
theorem main : MainStatement :=
…
```
Mentions: OAI.ComplexCancellation.MainStatement