Basic

📁 Source: Mathlib/Algebra/AddConstMap/Basic.lean

Statistics

Metric	Count
Definitions AddConstMap, addLeftHom, comp, conjNeg, id, instAddActionOfVAddAssocClass, instFunLike, instInhabited, instMonoid, instMul, instOne, instPowNat, instVAddOfVAddAssocClass, mkFract, replaceConsts, smul, toEnd, toFun, «term_→+c[_,_]_», AddConstMapClass	20
Theorems coe_addLeftHom_apply, coe_comp, coe_conjNeg_apply, coe_id, coe_mk, coe_mul, coe_one, coe_pow, coe_replaceConsts, coe_smul, coe_vadd, comp_id, conjNeg_symm, ext, ext_iff, id_comp, instAddConstMapClass, map_add_const', mk_coe, mul_def, one_def, pow_apply, toEnd_apply, toFun_eq_coe, antitone_iff_Icc, map_add_const, map_add_int, map_add_int', map_add_nat, map_add_nat', map_add_nsmul, map_add_ofNat, map_add_ofNat', map_add_one, map_add_zsmul, map_const, map_const_add, map_fract, map_int_add, map_int_add', map_nat, map_nat', map_nat_add, map_nat_add', map_nsmul_add, map_nsmul_const, map_ofNat, map_ofNat', map_ofNat_add, map_ofNat_add', map_one, map_one_add, map_sub_const, map_sub_int, map_sub_int', map_sub_nat', map_sub_nsmul, map_sub_ofNat', map_sub_one, map_sub_zsmul, map_zsmul_add, map_zsmul_const, monotone_iff_Icc, rel_map_of_Icc, semiconj, strictAnti_iff_Icc, strictMono_iff_Icc	67
Total	87

AddConstMap

Definitions

Name	Category	Theorems
addLeftHom 📖	CompOp	1 math math: coe_addLeftHom_apply
comp 📖	CompOp	4 math math: id_comp, coe_comp, mul_def, comp_id
conjNeg 📖	CompOp	2 math math: conjNeg_symm, coe_conjNeg_apply
id 📖	CompOp	4 math math: id_comp, one_def, coe_id, comp_id
instAddActionOfVAddAssocClass 📖	CompOp	—
instFunLike 📖	CompOp	21 math math: coe_addLeftHom_apply, toEnd_apply, coe_smul, pow_apply, ext_iff, AddConstEquiv.coe_val_inv_equivUnits_apply, coe_replaceConsts, coe_comp, coe_mul, AddConstEquiv.equivUnits_symm_apply_apply, coe_mk, coe_vadd, coe_id, toFun_eq_coe, AddConstEquiv.equivUnits_symm_apply_symm_apply, coe_conjNeg_apply, instAddConstMapClass, coe_pow, mk_coe, AddConstEquiv.coe_val_equivUnits_apply, coe_one
instInhabited 📖	CompOp	—
instMonoid 📖	CompOp	7 math math: coe_addLeftHom_apply, toEnd_apply, AddConstEquiv.toAddConstMapHom_apply, AddConstEquiv.coe_val_inv_equivUnits_apply, AddConstEquiv.equivUnits_symm_apply_apply, AddConstEquiv.equivUnits_symm_apply_symm_apply, AddConstEquiv.coe_val_equivUnits_apply
instMul 📖	CompOp	2 math math: coe_mul, mul_def
instOne 📖	CompOp	2 math math: one_def, coe_one
instPowNat 📖	CompOp	2 math math: pow_apply, coe_pow
instVAddOfVAddAssocClass 📖	CompOp	1 math math: coe_vadd
mkFract 📖	CompOp	—
replaceConsts 📖	CompOp	1 math math: coe_replaceConsts
smul 📖	CompOp	1 math math: coe_smul
toEnd 📖	CompOp	1 math math: toEnd_apply
toFun 📖	CompOp	2 math math: toFun_eq_coe, map_add_const'
«term_→+c[_,_]_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_addLeftHom_apply 📖	mathematical	—	DFunLike.coe AddConstMap AddSemigroup.toAdd AddMonoid.toAddSemigroup instFunLike MonoidHom Multiplicative MulOneClass.toMulOne Multiplicative.mulOneClass AddMonoid.toAddZeroClass Monoid.toMulOneClass instMonoid MonoidHom.instFunLike addLeftHom HVAdd.hVAdd instHVAdd Function.hasVAdd AddSemigroupAction.toVAdd AddAction.toAddSemigroupAction AddMonoid.toAddAction Equiv EquivLike.toFunLike Equiv.instEquivLike Multiplicative.toAdd	—	—
coe_comp 📖	mathematical	—	DFunLike.coe AddConstMap instFunLike comp	—	—
coe_conjNeg_apply 📖	mathematical	—	DFunLike.coe AddConstMap AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid instFunLike Equiv EquivLike.toFunLike Equiv.instEquivLike conjNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—
coe_id 📖	mathematical	—	DFunLike.coe AddConstMap instFunLike id	—	—
coe_mk 📖	mathematical	—	DFunLike.coe AddConstMap instFunLike	—	—
coe_mul 📖	mathematical	—	DFunLike.coe AddConstMap instFunLike instMul	—	—
coe_one 📖	mathematical	—	DFunLike.coe AddConstMap instFunLike instOne	—	—
coe_pow 📖	mathematical	—	DFunLike.coe AddConstMap instFunLike instPowNat Nat.iterate	—	—
coe_replaceConsts 📖	mathematical	—	DFunLike.coe AddConstMap instFunLike replaceConsts	—	—
coe_smul 📖	mathematical	—	DFunLike.coe AddConstMap AddZero.toAdd AddZeroClass.toAddZero SMulZeroClass.toSMul AddZero.toZero DistribSMul.toSMulZeroClass instFunLike smul Function.hasSMul	—	—
coe_vadd 📖	mathematical	—	DFunLike.coe AddConstMap instFunLike HVAdd.hVAdd instHVAdd instVAddOfVAddAssocClass Function.hasVAdd	—	—
comp_id 📖	mathematical	—	comp id	—	—
conjNeg_symm 📖	mathematical	—	Equiv.symm AddConstMap AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid conjNeg	—	—
ext 📖	—	DFunLike.coe AddConstMap instFunLike	—	—	DFunLike.ext
ext_iff 📖	mathematical	—	DFunLike.coe AddConstMap instFunLike	—	ext
id_comp 📖	mathematical	—	comp id	—	—
instAddConstMapClass 📖	mathematical	—	AddConstMapClass AddConstMap instFunLike	—	map_add_const'
map_add_const' 📖	mathematical	—	toFun	—	—
mk_coe 📖	mathematical	—	DFunLike.coe AddConstMap instFunLike map_add_const'	—	map_add_const'
mul_def 📖	mathematical	—	AddConstMap instMul comp	—	—
one_def 📖	mathematical	—	AddConstMap instOne id	—	—
pow_apply 📖	mathematical	—	DFunLike.coe AddConstMap instFunLike instPowNat Nat.iterate	—	—
toEnd_apply 📖	mathematical	—	DFunLike.coe MonoidHom AddConstMap Function.End MulOneClass.toMulOne Monoid.toMulOneClass instMonoid instMonoidEnd MonoidHom.instFunLike toEnd instFunLike	—	—
toFun_eq_coe 📖	mathematical	—	toFun DFunLike.coe AddConstMap instFunLike	—	—

AddConstMapClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
antitone_iff_Icc 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	Antitone DFunLike.coe AntitoneOn Set.Icc AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid	—	monotone_iff_Icc OrderDual.isOrderedAddMonoid AddCommGroup.add_comm
map_add_const 📖	mathematical	—	DFunLike.coe	—	—
map_add_int 📖	mathematical	—	DFunLike.coe AddSemigroup.toAdd AddMonoid.toAddSemigroup AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne AddGroupWithOne.toIntCast	—	map_add_int' zsmul_one
map_add_int' 📖	mathematical	—	DFunLike.coe AddSemigroup.toAdd AddMonoid.toAddSemigroup AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne AddGroupWithOne.toIntCast SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SubNegMonoid.toZSMul	—	map_add_zsmul zsmul_one
map_add_nat 📖	mathematical	—	DFunLike.coe AddSemigroup.toAdd AddMonoid.toAddSemigroup AddMonoidWithOne.toAddMonoid AddMonoidWithOne.toNatCast	—	map_add_nat' nsmul_one
map_add_nat' 📖	mathematical	—	DFunLike.coe AddSemigroup.toAdd AddMonoid.toAddSemigroup AddMonoidWithOne.toAddMonoid AddMonoidWithOne.toNatCast AddMonoid.toNatSMul	—	nsmul_one
map_add_nsmul 📖	mathematical	—	DFunLike.coe AddSemigroup.toAdd AddMonoid.toAddSemigroup AddMonoid.toNatSMul	—	add_right_iterate Function.Semiconj.iterate_right semiconj
map_add_ofNat 📖	mathematical	—	DFunLike.coe AddSemigroup.toAdd AddMonoid.toAddSemigroup AddMonoidWithOne.toAddMonoid	—	map_add_nat
map_add_ofNat' 📖	mathematical	—	DFunLike.coe AddSemigroup.toAdd AddMonoid.toAddSemigroup AddMonoidWithOne.toAddMonoid AddMonoid.toNatSMul	—	map_add_nat'
map_add_one 📖	mathematical	—	DFunLike.coe AddSemigroup.toAdd AddMonoid.toAddSemigroup AddMonoidWithOne.toAddMonoid AddMonoidWithOne.toOne	—	map_add_const
map_add_zsmul 📖	mathematical	—	DFunLike.coe AddSemigroup.toAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SubNegMonoid.toZSMul	—	natCast_zsmul map_add_nsmul negSucc_zsmul map_sub_nsmul
map_const 📖	mathematical	—	DFunLike.coe AddZero.toZero AddZeroClass.toAddZero	—	zero_add map_add_const
map_const_add 📖	mathematical	—	DFunLike.coe AddCommMagma.toAdd	—	add_comm map_add_const
map_fract 📖	mathematical	—	DFunLike.coe Int.fract SubNegMonoid.toSub AddGroup.toSubNegMonoid SubNegMonoid.toZSMul Int.floor	—	map_sub_int'
map_int_add 📖	mathematical	—	DFunLike.coe AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommMonoidWithOne.toAddCommMonoid AddCommGroupWithOne.toAddCommMonoidWithOne AddGroupWithOne.toIntCast AddCommGroupWithOne.toAddGroupWithOne AddSemigroup.toAdd AddMonoid.toAddSemigroup AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne	—	map_int_add' zsmul_one
map_int_add' 📖	mathematical	—	DFunLike.coe AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommMonoidWithOne.toAddCommMonoid AddCommGroupWithOne.toAddCommMonoidWithOne AddGroupWithOne.toIntCast AddCommGroupWithOne.toAddGroupWithOne AddSemigroup.toAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SubNegMonoid.toZSMul	—	map_zsmul_add zsmul_one
map_nat 📖	mathematical	—	DFunLike.coe AddMonoidWithOne.toNatCast AddSemigroup.toAdd AddMonoid.toAddSemigroup AddMonoidWithOne.toAddMonoid AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	map_nat' nsmul_one
map_nat' 📖	mathematical	—	DFunLike.coe AddMonoidWithOne.toNatCast AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddMonoid.toNatSMul	—	zero_add map_add_nat'
map_nat_add 📖	mathematical	—	DFunLike.coe AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommMonoidWithOne.toAddCommMonoid AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne AddSemigroup.toAdd AddMonoid.toAddSemigroup AddMonoidWithOne.toAddMonoid	—	map_nat_add' nsmul_one
map_nat_add' 📖	mathematical	—	DFunLike.coe AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommMonoidWithOne.toAddCommMonoid AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne AddSemigroup.toAdd AddMonoid.toAddSemigroup AddMonoid.toNatSMul	—	nsmul_one map_nsmul_add
map_nsmul_add 📖	mathematical	—	DFunLike.coe AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddMonoid.toNatSMul AddCommMonoid.toAddMonoid AddSemigroup.toAdd AddMonoid.toAddSemigroup	—	add_comm map_add_nsmul
map_nsmul_const 📖	mathematical	—	DFunLike.coe AddMonoid.toNatSMul AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	zero_add map_add_nsmul
map_ofNat 📖	mathematical	—	DFunLike.coe AddSemigroup.toAdd AddMonoid.toAddSemigroup AddMonoidWithOne.toAddMonoid AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	map_nat
map_ofNat' 📖	mathematical	—	DFunLike.coe AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddMonoid.toNatSMul	—	map_nat'
map_ofNat_add 📖	mathematical	—	DFunLike.coe AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommMonoidWithOne.toAddCommMonoid AddSemigroup.toAdd AddMonoid.toAddSemigroup AddMonoidWithOne.toAddMonoid	—	map_nat_add
map_ofNat_add' 📖	mathematical	—	DFunLike.coe AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommMonoidWithOne.toAddCommMonoid AddSemigroup.toAdd AddMonoid.toAddSemigroup AddMonoid.toNatSMul	—	map_nat_add'
map_one 📖	mathematical	—	DFunLike.coe AddZero.toZero AddZeroClass.toAddZero	—	map_const
map_one_add 📖	mathematical	—	DFunLike.coe AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommMonoidWithOne.toAddCommMonoid AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne	—	map_const_add
map_sub_const 📖	mathematical	—	DFunLike.coe SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	one_smul map_sub_nsmul
map_sub_int 📖	mathematical	—	DFunLike.coe SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup AddGroupWithOne.toIntCast	—	map_sub_int' zsmul_one
map_sub_int' 📖	mathematical	—	DFunLike.coe SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup AddGroupWithOne.toIntCast SubNegMonoid.toZSMul	—	map_sub_zsmul zsmul_one
map_sub_nat' 📖	mathematical	—	DFunLike.coe SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne AddMonoid.toNatSMul SubNegMonoid.toAddMonoid	—	nsmul_one map_sub_nsmul
map_sub_nsmul 📖	mathematical	—	DFunLike.coe SubNegMonoid.toSub AddGroup.toSubNegMonoid AddMonoid.toNatSMul SubNegMonoid.toAddMonoid	—	sub_add_cancel map_add_nsmul add_sub_cancel_right
map_sub_ofNat' 📖	mathematical	—	DFunLike.coe SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup AddMonoid.toNatSMul SubNegMonoid.toAddMonoid	—	map_sub_nat'
map_sub_one 📖	mathematical	—	DFunLike.coe SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	map_sub_const
map_sub_zsmul 📖	mathematical	—	DFunLike.coe SubNegMonoid.toSub AddGroup.toSubNegMonoid SubNegMonoid.toZSMul	—	sub_eq_add_neg neg_zsmul map_add_zsmul
map_zsmul_add 📖	mathematical	—	DFunLike.coe AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddSemigroup.toAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid	—	add_comm map_add_zsmul
map_zsmul_const 📖	mathematical	—	DFunLike.coe SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddSemigroup.toAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	zero_add map_add_zsmul
monotone_iff_Icc 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	Monotone DFunLike.coe MonotoneOn Set.Icc AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid	—	Monotone.monotoneOn monotone_iff_forall_lt rel_map_of_Icc instIsTransLe covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono LT.lt.le
rel_map_of_Icc 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid DFunLike.coe	Relator.LiftFun	—	CovariantClass.elim LT.lt.le existsUnique_sub_zsmul_mem_Ioc lt_trichotomy sub_le_iff_le_add covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono add_comm add_smul one_smul add_assoc add_le_add_right zsmul_le_zsmul_left le_of_lt zero_smul add_zero LT.lt.not_ge Set.Ico_subset_Icc_self sub_zero Set.Ioc_subset_Icc_self sub_add_cancel map_add_zsmul IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le LE.le.eq_or_lt zero_add Int.rel_of_forall_rel_succ_of_lt add_zsmul one_zsmul IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono existsUnique_sub_zsmul_mem_Ico IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd map_sub_zsmul
semiconj 📖	mathematical	—	Function.Semiconj DFunLike.coe	—	map_add_const
strictAnti_iff_Icc 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	StrictAnti DFunLike.coe StrictAntiOn Set.Icc AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid	—	strictMono_iff_Icc OrderDual.isOrderedAddMonoid AddCommGroup.add_comm
strictMono_iff_Icc 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	StrictMono DFunLike.coe StrictMonoOn Set.Icc AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid	—	StrictMono.strictMonoOn rel_map_of_Icc instIsTransLt IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono

(root)

Definitions

Name	Category	Theorems
AddConstMap 📖	CompData	25 math math: AddConstMap.conjNeg_symm, AddConstMap.coe_addLeftHom_apply, AddConstMap.toEnd_apply, AddConstMap.one_def, AddConstMap.coe_smul, AddConstEquiv.toAddConstMapHom_apply, AddConstMap.pow_apply, AddConstMap.ext_iff, AddConstEquiv.coe_val_inv_equivUnits_apply, AddConstMap.coe_replaceConsts, AddConstMap.coe_comp, AddConstMap.coe_mul, AddConstEquiv.equivUnits_symm_apply_apply, AddConstMap.mul_def, AddConstMap.coe_mk, AddConstMap.coe_vadd, AddConstMap.coe_id, AddConstMap.toFun_eq_coe, AddConstEquiv.equivUnits_symm_apply_symm_apply, AddConstMap.coe_conjNeg_apply, AddConstMap.instAddConstMapClass, AddConstMap.coe_pow, AddConstMap.mk_coe, AddConstEquiv.coe_val_equivUnits_apply, AddConstMap.coe_one
AddConstMapClass 📖	CompData	2 math math: AddConstEquiv.instAddConstMapClass, AddConstMap.instAddConstMapClass

---

← Back to Index