Theorems · Definition · ring theory

starRingEnd

(R : Type u) → [inst : CommSemiring R] → [StarRing R] → R →+* R

star as a ring endomorphism, for commutative R. This is used to denote complex conjugation, and is available under the notation conj in the scope ComplexConjugate. Note that this is the preferred form (over starRingAut, available under the same hypotheses) because the notation E →ₗ⋆[R] F for an R-conjugate-linear map (short for E →ₛₗ[starRingEnd R] F) does not pretty-print if there is a coercion involved, as would be the case for (↑starRingAut : R →* R).

Defined in

Mathlib.Algebra.Star.Basic

Cited by

671 results in Mathlib

Foundations

Depth 23 from the axioms, rests on 204 definitions · uses Quot.sound

Assumes

CommSemiringStarRing