`BookProof.ClosureUniqueness.eq_clExt_of_isClosureOf` {T : D →ₗ[ℂ] F} {A : Dom →ₗ[ℂ] F} (hA : IsClosureOf T A) (hdense : Dense (D : Set F)) (hsym : SymmetricOn D T) : Dom = clDom T

Initializing...

`BookProof.ClosureUniqueness.eq_clExt_of_isClosureOf` {T : D →ₗ[ℂ] F} {A : Dom →ₗ[ℂ] F} (hA : IsClosureOf T A) (hdense : Dense (D : Set F)) (hsym : SymmetricOn D T) : Dom = clDom T · Prove2Me