Revision #994 → #2512 · back to history
modifiedReal line as subalgebra of complex numbers6a7fb2024d3c
| Field | From #994 | To #2512 |
|---|
| mathlib.decl | Subalgebra.range | AlgHom.range |
| provenance | ai | ai-moderated |
modifiedMultiplication determined by basisc3019a1cfd78
| Field | From #994 | To #2512 |
|---|
| mathlib.decl | Basis.constr | Module.Basis.constr |
| provenance | ai | ai-moderated |
modifiedRing is associative algebra over its center78da87a19fda
| Field | From #994 | To #2512 |
|---|
| mathlib.decl | Algebra.instSubringCenter | Algebra.instSubtypeMemSubringCenter |
| provenance | ai | ai-moderated |