`BookProof.ClosureUniqueness.positive_sqrt_unique` {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (S B C : H →L[ℂ] H) (hB : B.IsPositive) (hC : C.IsPo

Initializing...

`BookProof.ClosureUniqueness.positive_sqrt_unique` {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (S B C : H →L[ℂ] H) (hB : B.IsPositive) (hC : C.IsPo · Prove2Me