Xavier Roblot

feat(algebra/order/complete.field): add real.ring_hom_eq_id

1

Proves that there are no nontrivial ring homomorphism from ℝ to ℝ. This is motivated by a remark of K. Buzzard (see https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Continuous.20complex.20ring.20hom/near/293264751). It looks like it should be a...

feat: add a version of `Ideal.associatesEquivIsPrincipal` for generators that are non-zero-divisors

1

This PR defines the following equiv: ```lean def Ideal.associatesNonZeroDivisorsEquivIsPrincipal : Associates R⁰ ≃ {I : (Ideal R)⁰ // IsPrincipal (I : Ideal R)} ``` Also, move the definition `Ideal.associatesEquivIsPrincipal` from...

feat(CanonicalEmbedding/FundamentalCone): Prove equivalence with principal ideals

1

--- - [ ] depends on: #12268 - [ ] depends on: #12780 [](https://gitpod.io/from-referrer/)

feat: two equiv involving `Associates` and `nonZeroDivisors`

2

This PR contains mainly the following two equivalences: ```lean def nonZeroDivisorsUnitsEquiv (α : Type*) [MonoidWithZero α] : (α⁰)ˣ ≃* αˣ ``` and ```lean def AssociatesNonZeroDivisorsMulEquiv (α : Type*) [CommMonoidWithZero α]...

feat(NumberField/CanonicalEmbedding): Define the fundamental cone for the action of the units of a number field

2

Let `K` be a number field of signature `(r₁, r₂)`. This PR defines an action of the group of units `(𝓞 K)ˣ` of `K` on the space `ℝ^r₁ × ℂ^r₂`...

This PR adds a new file `RingTheory.Ideal.IsPrincipal` and moves most of the (basic) results about `Ideal.IsPrincipal` and `Ideal.span_singleton` from `Ideal.Basic` and `Ideal.Operations` to this file. (Some very basic results or...

feat(Ideal.IsPrincipal): Prove that the equiv between principal ideals and associates is a `MulEquiv`

2

Define the `Submonoid` of principal ideals and prove that `associatesEquivIsPrincipal : Associates R ≃ {I : Ideal R // Submodule.IsPrincipal I}` actually yields a `MulEquiv` between `Associates R` and this...

feat(NumberTheory/NumberField): proof of the Analytic Class Number Formula

2

--- - [ ] depends on: #16675 - [x] depends on: #16822 - [ ] depends on: #12488 - [ ] depends on: #12405 - [x] depends on: #17943 -...

feat(NumberField/CanonicalEmbedding): put an euclidean space structure on the mixed space

1

This PR defines the natural euclidian space stucture on the mixed space `ℝ^r₁ × ℂ^r₂` of a number field of signature of `K` and the map between the `Euclidean.mixedSpace K`...

feat(NumberField/FundamentalCone): generalize the bijection to integral ideals

1

This PR is part of the proof of the Analytic Class Number Formula. --- [](https://gitpod.io/from-referrer/)