Skip to content

Commit adb1fa7

Browse files
committed
chore: add a shortcut Module ℂ ℂ instance for computability (leanprover-community#29609)
This makes the construction in [#new members > Defining an inner product to use Cauchy-Schwarz @ 💬](https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/Defining.20an.20inner.20product.20to.20use.20Cauchy-Schwarz/near/539179544) computable. Previously to make it computable, it could not be defined in the point-free way.
1 parent 71ded59 commit adb1fa7

1 file changed

Lines changed: 4 additions & 0 deletions

File tree

Mathlib/Analysis/Complex/Basic.lean

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -40,6 +40,10 @@ We also register the fact that `ℂ` is an `RCLike` field.
4040

4141
assert_not_exists Absorbs
4242

43+
/-- A shortcut instance to ensure computability; otherwise we get the noncomputable instance
44+
`Complex.instNormedField.toNormedModule.toModule`. -/
45+
instance Complex.instModuleSelf : Module ℂ ℂ := delta% inferInstance
46+
4347
noncomputable section
4448

4549
namespace Complex

0 commit comments

Comments
 (0)