Documentation

Mathlib.Analysis.Complex.IsIntegral

Integral elements of ℂ #

This file proves that Complex.I is integral over any commutative ring R when ℂ is an R-algebra.

source
theorem Complex.isIntegral_I (R : Type u_1) [CommRing R] [Algebra R ℂ] :
IsIntegral R I
source
@[deprecated Complex.isIntegral_I (since := "2026-08-06")]
theorem Complex.isIntegral_int_I (R : Type u_1) [CommRing R] [Algebra R ℂ] :
IsIntegral R I

Alias of Complex.isIntegral_I.

source
@[deprecated Complex.isIntegral_I (since := "2026-08-06")]
theorem Complex.isIntegral_rat_I (R : Type u_1) [CommRing R] [Algebra R ℂ] :
IsIntegral R I

Alias of Complex.isIntegral_I.