Theorems · Definition · functional analysis

ContinuousAlgEquiv.refl

(R : Type u_1) →
  (A : Type u_2) →
    [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : TopologicalSpace A] → [inst_3 : Algebra R A] → A ≃A[R] A

The identity isomorphism as a continuous R-algebra equivalence.

Defined in

Mathlib.Topology.Algebra.Algebra.Equiv

Cited by

31 results in Mathlib

Foundations

Depth 18 from the axioms · uses no axioms

Assumes

CommSemiringSemiringTopologicalSpaceAlgebra