Moritz Doll

The structure is taken literally from `linear_algebra/matrix/bilinear_form` with generalizations and easier proofs where possible. --- [](https://gitpod.io/from-referrer/)

refactor(analysis/inner_product_space): rename `is_self_adjoint` to `is_symmetric` and add `is_self_adjoint`

4

We rename the current `inner_product_space.is_self_adjoint` to `linear_map.is_symmetric` (which states that `inner (A x) y = inner x (A y)` for all `x,y : E`) and add a new definition `is_self_adjoint`...

I just open this to track my progress and let everyone know how I plan to do this. This is very tedious, so if anyone wants to help I would...

Pi is irrational

5

Prove that `real.pi` is irrational using [Niven's argument](https://projecteuclid.org/journals/bulletin-of-the-american-mathematical-society/volume-53/issue-6/A-simple-proof-that-pi-is-irrational/bams/1183510788.full), see also [Wikipedia](https://en.wikipedia.org/wiki/Proof_that_%CF%80_is_irrational#Niven's_proof) [Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Paulson's.20.22small.20formalisation.20challenges.22)

feat(analysis/locally_convex): the topology of a locally convex space is generated by seminorms

1

This PR provides the proof that every locally convex space has a family of seminorms that induces the topology. This PR also adds a new simp-lemma `is_R_or_C.real_norm`, which calculates the...

chore(analysis/inner_product_space/basic): remove `bilin_form_of_real_inner`

3

Remove `bilin_form_of_real_inner` and add a remark in the docstring of `sesq_form_of_inner` that for over real spaces the sesquilinear form is by definition a bilinear form. For this we generalize `is_self_adjoint_iff_bilin_form`...

chore: simplify proofs using new positivity extensions and tests

1

--- - [x] depends on: #10661 - [ ] depends on: #10796 [](https://gitpod.io/from-referrer/)