Structures · Algebra
AlgEquivClass
AlgEquivClass F R A B states that F is a type of algebra structure preserving
equivalences. You should extend this class when you extend AlgEquiv.
- Defined in
- Mathlib.Algebra.Algebra.Equiv
- Shape
- 4 explicit arguments · adds commutes
Extends1
Extended by1
Concrete types that are instances2
- AlgEquiv
- Polynomial.Gal
How is a type an instance?
Loading the hierarchy index…
Assumed by25
- AlgEquivClass.toAlgEquiv
- AlgEquiv.spectrum_eq
- Matrix.det_map
- Ideal.Quotient.algEquivOfEqComap
- Ideal.inertiaDeg'_map_eq
- LinearMap.trace_map
- LinearMap.det_map
- Ideal.Quotient.algEquivOfEqMap
- Ideal.ramificationIdx'_map_eq
- Matrix.trace_map
- AlgEquiv.coe_coe_symm_apply_coe_apply
- AlgEquivClass.toAlgEquiv.congr_simp
- AlgEquivClass.commutes
- AlgEquivClass.toAlgHomClass
- Ideal.map_equiv_liesOver
- Ideal.ramificationIdx_map_eq
- AlgEquiv.coe_apply_coe_coe_symm_apply
- AlgEquivClass.toRingEquivClass
- Ideal.LiesOver.of_eq_map_equiv
- Ideal.Quotient.algEquivOfEqComap_apply
- AlgEquiv.coe_coe
- Ideal.Quotient.algEquivOfEqMap_apply
- NumberField.RingOfIntegers.mapAlgEquiv
- AlgEquivClass.toLinearEquivClass
- Ideal.inertiaDeg_map_eq