Revision #1544 → #2642 · back to history
modifiedContinuous real-valued functionse634d2e17a7b
| Field | From #1544 | To #2642 |
|---|
| mathlib.decl | ContinuousMap.instCommRing | ContinuousMap.instCommRingOfIsTopologicalRing |
| provenance | ai | ai-moderated |
modifiedCommutative simple rings are fields62dffa8b5517
| Field | From #1544 | To #2642 |
|---|
| mathlib.decl | IsSimpleRing.isField | isSimpleRing_iff_isField |
| provenance | ai | ai-moderated |
modifiedQuotient ring9c610af678f8
| Field | From #1544 | To #2642 |
|---|
| mathlib.decl | Ideal.Quotient | Ideal.Quotient.mk |
| provenance | ai | ai-moderated |
modifiedFinite direct product as direct sum of ideals0c45f7b7b9af
| Field | From #1544 | To #2642 |
|---|
| mathlib.decl | Ideal.CompleteOrthogonalIdempotents | CompleteOrthogonalIdempotents |
| provenance | ai | ai-moderated |
modifiedProperties of polynomial ringsf63396ca87e3
| Field | From #1544 | To #2642 |
|---|
| mathlib.decl | Polynomial.instIsDomain | Polynomial.instIsDomainOfIsCancelAdd |
| provenance | ai | ai-moderated |
modifiedSchur's lemmad0e42b4f5190
| Field | From #1544 | To #2642 |
|---|
| mathlib.decl | IsSimpleModule.instDivisionRingEnd | Module.End.instDivisionRing |
| provenance | ai | ai-moderated |
modifiedProjective limit of rings78243f1f2c46
| Field | From #1544 | To #2642 |
|---|
| mathlib.decl | CommRingCat.HasLimits | CommRingCat.hasLimits |
| provenance | ai | ai-moderated |
modifiedExactness from local exactnessd3320e6bd8c6
| Field | From #1544 | To #2642 |
|---|
| mathlib.decl | Module.exact_of_localization_maximal | exact_of_localized_maximal |
| provenance | ai | ai-moderated |
modifiedTensor product of algebrasb4a73ec2c36d
| Field | From #1544 | To #2642 |
|---|
| mathlib.decl | Algebra.TensorProduct | Algebra.TensorProduct.instAlgebra |
| provenance | ai | ai-moderated |
modifiedWedderburn's little theoremfdb20438ef8e
| Field | From #1544 | To #2642 |
|---|
| mathlib.decl | LittleWedderburn | littleWedderburn |
| provenance | ai | ai-moderated |
modifiedMatrix ring over a division ring is semisimplebc54799a3b73
| Field | From #1544 | To #2642 |
|---|
| mathlib.decl | Matrix.instIsSemisimpleRing | IsSemisimpleRing.instMatrix |
| provenance | ai | ai-moderated |
modifiedRing as monoid in Ab0d434173972a
| Field | From #1544 | To #2642 |
|---|
| mathlib.decl | Mon_Class | CategoryTheory.MonObj |
| provenance | ai | ai-moderated |
modifiedRing object in a categorycc5035296e75
| Field | From #1544 | To #2642 |
|---|
| mathlib.decl | Mon_Class | CategoryTheory.MonObj |
| provenance | ai | ai-moderated |