Normed multiplicative bases along algebra isomorphisms

Corollary 5.5(2) (mesh-deformations.tex): "The ray basis transports to a normed multiplicative basis of A." An algebra isomorphism preserves products, idempotents, primitivity and the radical powers, so it transports normed multiplicative bases (HasNormedMultiplicativeBasis.of_algEquiv).

theorem MultiplicativeBasisDeformations.jacobson_map_mem {A B : Type v} [Ring A] [Ring B] (φ : A ≃+* B) {x : A} (hx : x ∈ Ring.jacobson A) : φ x ∈ Ring.jacobson B

theorem MultiplicativeBasisDeformations.map_algebraRadical {k : Type u} [Field k] {A B : Type v} [Ring A] [Ring B] [Algebra k A] [Algebra k B] (φ : A ≃ₐ[k] B) : Submodule.map φ.toLinearMap (algebraRadical k A) = algebraRadical k B

theorem MultiplicativeBasisDeformations.map_algebraRadicalPow {k : Type u} [Field k] {A B : Type v} [Ring A] [Ring B] [Algebra k A] [Algebra k B] (φ : A ≃ₐ[k] B) (n : ℕ) : Submodule.map φ.toLinearMap (algebraRadicalPow k A n) = algebraRadicalPow k B n

theorem MultiplicativeBasisDeformations.isPrimitiveIdempotent_map {k : Type u} [Field k] {A B : Type v} [Ring A] [Ring B] [Algebra k A] [Algebra k B] (φ : A ≃ₐ[k] B) {x : A} (hx : IsPrimitiveIdempotent x) : IsPrimitiveIdempotent (φ x)

theorem MultiplicativeBasisDeformations.HasNormedMultiplicativeBasis.of_algEquiv {k : Type u} [Field k] {A B : Type v} [Ring A] [Ring B] [Algebra k A] [Algebra k B] (φ : A ≃ₐ[k] B) (h : HasNormedMultiplicativeBasis k B) : HasNormedMultiplicativeBasis k A

Transport of normed multiplicative bases.