Mathlib Map

Theorems · Definition · ring theory

WithConv.ofConv

{A : Sort u_1} → WithConv A → A

Converts an element of WithConv A back to A.

Defined in
Mathlib.Algebra.WithConv
Cited by
97 results in Mathlib
Foundations
Depth 1 from the axioms, rests on 2 definitions · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

WithConv.ext · cited by 25WithConv.extWithConv.ofConv_injective · cited by 4WithConv.ofConv_injectiveWithConv.equiv · cited by 3WithConv.equivWithConv.ofConv_toConv · cited by 3WithConv.ofConv_toConvCoalgebra.Repr.convMul_apply · cited by 3Repr.convMul_applyLinearMap.toMatrix'_intrinsicStar · cited by 2LinearMap.toMatrix'_intri…TensorProduct.intrinsicStar_map · cited by 2TensorProduct.intrinsicSt…Matrix.intrinsicStar_toLin' · cited by 2Matrix.intrinsicStar_toLi…AlgHom.toLinearMap_convMul · cited by 2AlgHom.toLinearMap_convMulWithConv.toConv_ofConv · cited by 2WithConv.toConv_ofConvAlgHom.convMul_apply · cited by 2AlgHom.convMul_applyTensorProduct.star_map_apply_eq_map_intrinsicStar · cited by 1TensorProduct.star_map_ap…LinearMap.id_mul_antipode · cited by 1LinearMap.id_mul_antipodePi.intrinsicStar_comul · cited by 1Pi.intrinsicStar_comulHopfAlgebra.antipode_comp_mul_comp_comm · cited by 1HopfAlgebra.antipode_comp…WithConv · cited by 138WithConvWithConv.ofConvCITED BYCITES

Cites1

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • WithConvstatement and proof · cited by 138

Cited by99

Results whose statement or proof uses this declaration.