Ultrapower (source code)

= Ultrapower
{title2=$M^I/\mathcal U$}

An ultrapower is an <ultraproduct> whose factors are all one structure $M$. Its elements are equivalence classes $[f]$ of functions $f:I\to M$, where $f\sim g$ exactly when $\{i\in I:f(i)=g(i)\}$ belongs to the chosen <ultrafilter> $\mathcal U$.