PositiveFunctionalExtension.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Positive functional extension along an injective unital star homomorphism, including the zero functional. This is the scalar extension used in the finite matrix extension construction.

theorem OAI.WeakPureInfiniteness.positiveFunctional_extension line 17