Revision #1328 → #2029 · back to history
modifiedAutomorphism79e931317e1a
| Field | From #1328 | To #2029 |
|---|
| mathlib.module | Mathlib.CategoryTheory.Iso | Mathlib.CategoryTheory.Endomorphism |
| note | Automorphisms appear generally as `Aut X := X ≅ X` in category theory, and as `Equiv.Perm`, `MulAut`, `RingAut`, etc. for specific structures. | Automorphisms appear generally as `Aut X := X ≅ X` in `Mathlib.CategoryTheory.Endomorphism`, and as `Equiv.Perm`, `MulAut`, `RingAut`, etc. for specific structures. |
modifiedLogarithm and exponential as group isomorphismsf3b00c3fd702
| Field | From #1328 | To #2029 |
|---|
| mathlib.module | Mathlib.Analysis.SpecialFunctions.Log.Basic | Mathlib.Analysis.SpecialFunctions.Exp |
| note | `Real.expOrderIso` packages exp/log as an order isomorphism ℝ ≃o ℝ>0, but a bundled `MulEquiv` between the additive reals and multiplicative positive reals via exp/log is not directly present. | `Real.expOrderIso` packages exp as an order isomorphism ℝ ≃o ℝ>0, but a bundled `MulEquiv`/`AddEquiv` between the additive reals and multiplicative positive reals via exp/log is not directly present. |
addedLinear isomorphism0c745cf702ce
addedGroup isomorphismca1b7c82b975
addedRing isomorphismae08c6884174
addedField isomorphism as ring isomorphism6518e57e7637
addedAutomorphisms form a groupbae2fc9b90f6
modifiedIsomorphism classes of sets86c7b287f95d
| Field | From #1328 | To #2029 |
|---|
| mathlib.module | Mathlib.SetTheory.Cardinal.Basic | Mathlib.SetTheory.Cardinal.Defs |
modifiedIsomorphism class of finite-dimensional vector spaceb7ebb11138b3
| Field | From #1328 | To #2029 |
|---|
| mathlib.module | Mathlib.LinearAlgebra.FiniteDimensional.Lemmas | Mathlib.LinearAlgebra.Dimension.Free |
modifiedOrdinals as isomorphism classes of well-ordered setsaa49d4f759dc
| Field | From #1328 | To #2029 |
|---|
| note | `Ordinal` is defined as the quotient of `WellOrder` by order-isomorphism via `Ordinal.isEquivalent`. | `Ordinal` is defined as the quotient of `WellOrder` by order-isomorphism. |
modifiedFundamental group base point dependence8a63631a8f9d
| Field | From #1328 | To #2029 |
|---|
| mathlib.module | Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic | Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup |
modifiedUniversal property gives unique isomorphism of rationals1a8f6c3b7eba
| Field | From #1328 | To #2029 |
|---|
| mathlib.decl | Rat.castRingHom | RingHom.ext_rat |
| mathlib.module | Mathlib.Algebra.Algebra.Rat | Mathlib.Data.Rat.Cast.Defs |
| note | Mathlib has unique ring homomorphisms from ℚ into any characteristic-zero field via `Rat.castRingHom` and `RingHom.ext_rat`, capturing ℚ's initial-object property among characteristic-zero fields, but a stand-alone universal-property uniqueness theorem isn't packaged. | `RingHom.ext_rat` gives uniqueness of ring homomorphisms out of ℚ, capturing ℚ's initial-object property among characteristic-zero fields, but a stand-alone universal-property uniqueness theorem packaging the field iso isn't present. |