feat(QuantumMechanics): Resolvent identities

[gloges]

Adds the following two resolvent identities:

• R T₁ z - R T₂ z = R T₁ z * (T₂ - T₁) * R T₂ z
• R T z₁ - R T z₂ = (z₁ - z₂) • (R T z₁ * R T z₂)

To do this requires first fleshing out more properties of compRestricted:

• Distributivity: (g₁ + g₂) ∘ᵣ f = g₁ ∘ᵣ f + g₂ ∘ᵣ f and g ∘ᵣ (f₁ + f₂) ≥ g ∘ᵣ f₁ + g ∘ᵣ f₂,
• Scalar multiplication: (c • g) ∘ᵣ f = c • (g ∘ᵣ f) = g ∘ᵣ (c • f) (the latter requires c ≠ 0),
• Inverses: f⁻¹ ∘ᵣ f = 1 and f ∘ᵣ f⁻¹ = 1 (with appropriate domain restrictions of "1").

[gloges]

t-quantum-mechanics

[github-actions]

Thank you for this PR, which will now be reviewed. Please
see our review guidelines
if you are not familiar with the process. You should expect a back and forth
with a reviewer before your PR is merged. See also that link for how to
add appropriate labels to your PR. The PR will also go through a number
of automated checks. You can learn more about these here,
including how to run them locally.

If you want to bring attention to this PR, please write a message on this
thread of the Lean Zulip.

[jstoobysmith]

Approved - looks good to me.