Opposite

📁 Source: Mathlib/Algebra/Module/Opposite.lean

Statistics

Metric	Count
Definitions instModule, toOppositeModule	2
Theorems	0
Total	2

MulOpposite

Definitions

Name	Category	Theorems
instModule 📖	CompOp	65 math math: coe_opLinearEquiv_symm, Submodule.comap_op_mul, Submodule.comap_op_pow, CategoryTheory.Preadditive.homSelfLinearEquivEndMulOpposite_apply, Submodule.LinearDisjoint.op, AlgHom.mulLeftRightMatrix.inv_comp, coe_opLinearEquiv_symm_addEquiv, Subalgebra.LinearDisjoint.linearIndependent_left_op_of_flat, Module.Basis.mulOpposite_apply, Module.Basis.mulOpposite_is_orthonormal_iff, AlgHom.toLinearMap_toOpposite, finrank, Submodule.map_unop_mul, coe_opLinearEquiv_addEquiv, instFree, isometry_opLinearEquiv, Algebra.TensorProduct.opAlgEquiv_apply, IsAzumaya.mulLeftRight_comp_congr, AlgHom.mulLeftRight_apply, IsAzumaya.bij, Module.Basis.mulOpposite_repr_op, opContinuousLinearEquiv_symm_apply, Submodule.map_unop_pow, Submodule.equivOpposite_apply, counit_def, coe_opLinearEquiv_toLinearMap, Submodule.map_op_pow, toLinearEquiv_opLinearIsometryEquiv, opLinearEquiv_toAddEquiv, Module.Finite.instMulOpposite, IsAzumaya.coe_tensorEquivEnd, Algebra.TensorProduct.opAlgEquiv_symm_apply, Submodule.linearDisjoint_op, CliffordAlgebra.toBaseChange_comp_reverseOp, opLinearIsometryEquiv_symm_apply, Submodule.map_op_mul, AlgHom.toLinearMap_fromOpposite, Submodule.map_unop_one, Module.Basis.mulOpposite_repr_eq, CategoryTheory.Preadditive.homSelfLinearEquivEndMulOpposite_symm_apply, opLinearIsometryEquiv_apply, Submodule.comap_unop_pow, rank, instFiniteDimensional, Algebra.TensorProduct.opAlgEquiv_tmul, TwoSidedIdeal.subtypeMop_apply, coe_opLinearEquiv, comul_def, opLinearEquiv_symm_toAddEquiv, opContinuousLinearEquiv_apply, Submodule.equivOpposite_symm_apply, toContinuousLinearEquiv_opLinearIsometryEquiv, Submodule.comap_unop_one, Submodule.mulMap_op, TwoSidedIdeal.subtypeMop_injective, coe_opLinearEquiv_symm_toLinearMap, Submodule.comap_op_one, instModuleIsReflexive, Submodule.map_op_one, Algebra.TensorProduct.opAlgEquiv_symm_tmul, Subalgebra.LinearDisjoint.mulLeftMap_ker_eq_bot_iff_linearIndependent_op, Submodule.comap_unop_mul, Module.Basis.repr_unop_eq_mulOpposite_repr, AlgHom.mulLeftRightMatrix.comp_inv, IsAzumaya.AlgHom.mulLeftRight_bij

Semiring

Definitions

Name	Category	Theorems
toOppositeModule 📖	CompOp	128 math math: HasStrictFDerivAt.fun_mul', AlgEquiv.moduleEndSelfOp_apply_apply, Quaternion.snd_imJ_dualNumberEquiv_symm, hasStrictFDerivAt_list_prod_finRange', Matrix.toLinearMapRight'_mul, fderivWithin_fun_pow', LinearMap.ext_ring_op_iff, DualNumber.range_lift, CliffordAlgebraDualNumber.equiv_symm_eps, CategoryTheory.Preadditive.homSelfLinearEquivEndMulOpposite_apply, Quaternion.snd_re_dualNumberEquiv_symm, HasStrictFDerivAt.mul', isLinearTopology_iff_hasBasis_open_twoSidedIdeal, Quaternion.imJ_fst_dualNumberEquiv, fderiv_fun_pow', Quaternion.imI_fst_dualNumberEquiv, DualNumber.lift_apply_eps, Subalgebra.LinearDisjoint.linearIndependent_left_op_of_flat, Matrix.toLinearEquivRight'OfInv_symm_apply, DualNumber.inv_eps, HasStrictFDerivAt.list_prod', MvPowerSeries.substAlgHom_eq_aeval, NormMulClass.toNormSMulClass_op, rank_lt_rank_dual', Quaternion.fst_imK_dualNumberEquiv_symm, fderiv_mul_const', DualNumber.fst_eq_zero_iff_eps_dvd, DualNumber.maximalIdeal_eq_span_singleton_eps, DualNumber.lift_inlAlgHom_eps, DualNumber.isNilpotent_iff_eps_dvd, DualNumber.isMaximal_span_singleton_eps, fderiv_pow', MvPowerSeries.LinearTopology.instIsLinearTopologyMulOpposite, DualNumber.lift_smul, Quaternion.imK_fst_dualNumberEquiv, lift_rank_lt_rank_dual', Quaternion.re_fst_dualNumberEquiv, RingEquiv.moduleEndSelfOp_apply, fderivWithin_fun_mul', hasFDerivAt_list_prod', Matrix.toLinearMapRight'_mul_apply, fderiv_mul', instIsTorsionFreeMulOpposite, DualNumber.exists_mul_left_or_mul_right, hasFDerivWithinAt_pow', RingEquiv.moduleEndSelf_apply, fderivWithin_mul_const', hasFDerivAt_list_prod_finRange', Quaternion.fst_imJ_dualNumberEquiv_symm, HasFDerivWithinAt.mul_const', Matrix.dualNumberEquiv_symm_apply, IsLinearTopology.instMulOpposite, DualNumber.exp_eps, IsTopologicalSemiring.toOppositeIsModuleTopology, fderiv_pow_ring', Quaternion.fst_imI_dualNumberEquiv_symm, rank_dual_eq_card_dual_of_aleph0_le_rank', HasFDerivAt.fun_pow', HasMFDerivWithinAt.mul', DualNumber.lift_apply_apply, LinearMap.toMatrixRight'_id, hasStrictFDerivAt_pow', DualNumber.coe_lift_symm_apply, Quaternion.imJ_snd_dualNumberEquiv, fderiv_fun_mul', Quaternion.snd_imK_dualNumberEquiv_symm, hasStrictFDerivAt_list_prod_attach', Matrix.scalar_comm_iff, DualNumber.range_inlAlgHom_sup_adjoin_eps, Matrix.toLinearMapRight'_apply, HasFDerivWithinAt.pow', HasFDerivAt.list_prod', hasFDerivAt_pow', DualNumber.commute_eps_left, DualNumber.algHom_ext_iff, CategoryTheory.Preadditive.homSelfLinearEquivEndMulOpposite_symm_apply, CliffordAlgebraDualNumber.equiv_ι, AlgEquiv.moduleEndSelfOp_symm_apply, DualNumber.commute_eps_right, DualNumber.instIsLocalRing, Matrix.toLinearEquivRight'OfInv_apply, HasFDerivAt.pow', HasStrictFDerivAt.pow', HasStrictFDerivAt.mul_const', Matrix.dualNumberEquiv_apply, fderivWithin_list_prod', HasFDerivWithinAt.fun_mul', Quaternion.re_snd_dualNumberEquiv, fderivWithin_pow_ring', TwoSidedIdeal.subtypeMop_apply, HasFDerivWithinAt.fun_pow', DualNumber.exp_smul_eps, Quaternion.snd_imI_dualNumberEquiv_symm, HasFDerivAt.mul_const', HasStrictFDerivAt.fun_pow', DualNumber.lift_apply_inl, DualNumber.lift_op_smul, PowerSeries.substAlgHom_eq_aeval, DualNumber.lift_comp_inlHom, DualNumber.algHom_ext'_iff, hasStrictFDerivAt_list_prod', TwoSidedIdeal.subtypeMop_injective, DualNumber.ideal_trichotomy, Ring.uniformContinuousConstSMul_op, DualNumber.eps_mul_eps, Matrix.toLinearMapRight'_one, HasFDerivWithinAt.mul', DualNumber.snd_mul, fderivWithin_mul', Matrix.scalar_commute_iff, fderiv_list_prod', HasMFDerivAt.mul', isLinearTopology_iff_hasBasis_twoSidedIdeal, Subalgebra.LinearDisjoint.mulLeftMap_ker_eq_bot_iff_linearIndependent_op, DualNumber.instIsPrincipalIdealRing, HasFDerivAt.fun_mul', HasFDerivAt.mul', Quaternion.fst_re_dualNumberEquiv_symm, hasFDerivAt_list_prod_attach', Quaternion.imI_snd_dualNumberEquiv, LinearMap.toMatrixRight'_comp, IsLinearTopology.hasBasis_right_ideal, DualNumber.isNilpotent_eps, RingEquiv.moduleEndSelfOp_symm_apply, HasFDerivWithinAt.list_prod', Quaternion.imK_snd_dualNumberEquiv, TwoSidedIdeal.coe_mop_smul, fderivWithin_pow'

---

← Back to Index