`BookProof.SmCar.norm_fermiBilin_le` (h : Matrix (Fin n) (Fin n) ℂ) (ψ : FermiFock n) : ‖fermiBilin h ψ‖ ≤ (∑ i : Fin n, ∑ j : Fin n, ‖h i j‖) * ‖ψ‖

Initializing...

`BookProof.SmCar.norm_fermiBilin_le` (h : Matrix (Fin n) (Fin n) ℂ) (ψ : FermiFock n) : ‖fermiBilin h ψ‖ ≤ (∑ i : Fin n, ∑ j : Fin n, ‖h i j‖) * ‖ψ‖ · Prove2Me