Revision #3632 → #4179 · back to history
modifiedProjective linear group via second isomorphism theorema10c0c3bf4ae
| Field | From #3632 | To #4179 |
|---|
| note | Mathlib defines `Matrix.ProjGenLinGroup` as `GL n R ⧸ Subgroup.center (GL n R)` directly, without deriving it as an instance of the second isomorphism theorem. | Verified: Mathlib defines `Matrix.ProjGenLinGroup` as `GL n R ⧸ Subgroup.center (GL n R)` directly, without deriving it as an instance of the second isomorphism theorem. |
modifiedSplitting lemma24fe170de933
| Field | From #3632 | To #4179 |
|---|
| note | Mathlib provides `CategoryTheory.ShortComplex.Splitting` in abelian categories, encoding the classical left/right split equivalence through the general splitting API rather than as a single named lemma. | Verified: Mathlib provides `CategoryTheory.ShortComplex.Splitting` in abelian categories, encoding the classical left/right split equivalence through the general splitting API rather than as a single named lemma. |
modifiedCorrespondence theorem (rings)232c0192081c
| Field | From #3632 | To #4179 |
|---|
| note | Verified: `Ideal.relIsoOfSurjective` gives the order iso `Ideal S ≃o {p : Ideal R // comap f ⊥ ≤ p}` for a surjective ring homomorphism. | Verified: `Ideal.relIsoOfSurjective` gives the order iso between ideals of `S` and ideals of `R` containing `ker f` for a surjective ring homomorphism. |
modifiedSecond isomorphism theorem (universal algebra)7651002936e1
| Field | From #3632 | To #4179 |
|---|
| note | Only structure-specific versions (`Con.comapQuotientEquiv`, `RingCon.comapQuotientEquivRange`, `LinearMap.quotientInfEquivSupQuotient`) are formalized. | Verified: only structure-specific versions (`Con.comapQuotientEquiv`, `RingCon.comapQuotientEquivRange`, `LinearMap.quotientInfEquivSupQuotient`) are formalized. |
modifiedSemidirect product from right-split short exact sequence1a8b57f236c5
| Field | From #3632 | To #4179 |
|---|
| note | Mathlib defines `SemidirectProduct` and provides the equivalence between a right-split short exact sequence of groups and a semidirect-product decomposition, though not packaged as a single named theorem matching this exact statement. | Verified: Mathlib defines `SemidirectProduct` and provides the equivalence between a right-split short exact sequence of groups and a semidirect-product decomposition, though not packaged as a single named theorem matching this exact statement. |