mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(analysis/inner_product_space/two_dim): the case of `ℂ`

Open hrmacbeth opened this issue 2 years ago • 1 comments

This file relates the constructions orientation.area_form, orientation.right_angle_rotation, orientation.kahler on an oriented two-dimensional real inner product space to their concrete interpretations over ℂ.

Open in Gitpod

  • [x] depends on: #16928

hrmacbeth avatar Oct 12 '22 13:10 hrmacbeth

This PR/issue depends on:

  • ~~leanprover-community/mathlib#16928~~ By Dependent Issues (🤖). Happy coding!

mathlib-dependent-issues-bot avatar Oct 13 '22 22:10 mathlib-dependent-issues-bot

maintainer merge

jsm28 avatar Oct 19 '22 21:10 jsm28

🚀 Pull request has been placed on the maintainer queue by jsm28.

github-actions[bot] avatar Oct 19 '22 21:10 github-actions[bot]

bors r+

sgouezel avatar Oct 20 '22 06:10 sgouezel

Pull request successfully merged into master.

Build succeeded:

bors[bot] avatar Oct 20 '22 08:10 bors[bot]