Theorems · Definition · linear algebra
Complex.conjAe
Gal(ℂ/ℝ)
ℝ-algebra isomorphism version of the complex conjugation function from ℂ to ℂ
- Defined in
- Mathlib.LinearAlgebra.Complex.Module
- Cited by
- 16 results in Mathlib
- Foundations
- Depth 109 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Realstatement · cited by 25,697
- RingHomproof · cited by 10,189
- Complexstatement and proof · cited by 5,565
- AlgEquivstatement · cited by 1,681
- starRingEndproof · cited by 671
- MonoidHom.toOneHomproof · cited by 132
- RingHom.toMonoidHomproof · cited by 132
- OneHom.toFunproof · cited by 132
- Complex.conj_ofRealproof · cited by 41
Cited by18
Results whose statement or proof uses this declaration.
- Complex.conjCAEproof · cited by 27
- Complex.conjLIEproof · cited by 12
- Complex.det_conjAestatement and proof · cited by 3
- Polynomial.Gal.card_complex_roots_eq_card_real_add_card_not_gal_invstatement and proof · cited by 2
- Complex.linearEquiv_det_conjAestatement · cited by 1
- Complex.toMatrix_conjAestatement and proof · cited by 1
- CliffordAlgebraComplex.toComplex_involuteproof · cited by 1
- Complex.real_algHom_eq_id_or_conjstatement · cited by 1
- ModularGroup.tendsto_normSq_coprime_pairproof · cited by 1
- Polynomial.Gal.galActionHom_bijective_of_prime_degreeproof · cited by 1
- Complex.liftAux_neg_Istatement · cited by 0
- UpperHalfPlane.det_smulFDerivproof · cited by 0