IntegerCompl

📁 Source: Mathlib/Analysis/Complex/IntegerCompl.lean

Statistics

Metric	Count
Definitions integerComplement	1
Theorems add_intCast_mem_integerComplement, add_coe_int_mem, mem_iff, ne_one, ne_zero, integerComplement_add_ne_zero, integerComplement_eq, integerComplement_pow_two_ne_pow_two, mem_integerComplement_iff, upperHalfPlane_inter_integerComplement, coe_mem_integerComplement, int_div_mem_integerComplement	12
Total	13

Complex

Definitions

Name	Category	Theorems
integerComplement 📖	CompOp	11 math math: mem_integerComplement_iff, UpperHalfPlane.int_div_mem_integerComplement, integerComplement.add_coe_int_mem, UpperHalfPlane.coe_mem_integerComplement, HasProdLocallyUniformlyOn_euler_sin_prod, eqOn_iteratedDeriv_cotTerm, integerComplement_eq, eqOn_iteratedDerivWithin_cotTerm_integerComplement, upperHalfPlane_inter_integerComplement, add_intCast_mem_integerComplement, integerComplement.mem_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_intCast_mem_integerComplement 📖	mathematical	—	Complex Set Set.instMembership integerComplement instAdd instIntCast	—	Int.cast_sub add_sub_cancel_right Int.cast_add
integerComplement_add_ne_zero 📖	—	Complex Set Set.instMembership integerComplement	—	—	integerComplement.ne_zero add_intCast_mem_integerComplement
integerComplement_eq 📖	mathematical	—	integerComplement setOf Complex instIntCast	—	—
integerComplement_pow_two_ne_pow_two 📖	—	Complex Set Set.instMembership integerComplement	—	—	NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Int.cast_neg
mem_integerComplement_iff 📖	mathematical	—	Complex Set Set.instMembership integerComplement instIntCast	—	—
upperHalfPlane_inter_integerComplement 📖	mathematical	—	Set Complex Set.instInter setOf Real Real.instLT Real.instZero im integerComplement	—	Set.inter_eq_self_of_subset_left UpperHalfPlane.coe_mem_integerComplement

Complex.integerComplement

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_coe_int_mem 📖	mathematical	—	Complex Set Set.instMembership Complex.integerComplement Complex.instAdd Complex.instIntCast	—	Complex.add_intCast_mem_integerComplement
mem_iff 📖	mathematical	—	Complex Set Set.instMembership Complex.integerComplement Complex.instIntCast	—	Complex.mem_integerComplement_iff
ne_one 📖	—	Complex Set Set.instMembership Complex.integerComplement	—	—	Nat.cast_one Int.cast_one
ne_zero 📖	—	Complex Set Set.instMembership Complex.integerComplement	—	—	Nat.cast_zero Int.cast_zero

UpperHalfPlane

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_mem_integerComplement 📖	mathematical	—	Complex Set Set.instMembership Complex.integerComplement coe	—	ne_intCast
int_div_mem_integerComplement 📖	mathematical	—	Complex Set Set.instMembership Complex.integerComplement DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instIntCast coe	—	Complex.div_im MulZeroClass.zero_mul zero_div zero_sub NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass RCLike.charZero_rclike im_ne_zero Real.instNontrivial MonoidWithZeroHom.monoidWithZeroHomClass ne_zero

---

← Back to Index