`BookProof.KatoRellich.deficiencyTrivialAt_of_dense` (T : D →ₗ[ℂ] F) (z : ℂ) (hd : Dense (Set.range fun x : D => T x - ((starRingEnd ℂ) z) • (x : F))) : DeficiencyTrivialAt D T z

Initializing...

`BookProof.KatoRellich.deficiencyTrivialAt_of_dense` (T : D →ₗ[ℂ] F) (z : ℂ) (hd : Dense (Set.range fun x : D => T x - ((starRingEnd ℂ) z) • (x : F))) : DeficiencyTrivialAt D T z · Prove2Me