FreimanHom

📁 Source: Mathlib/Combinatorics/Additive/FreimanHom.lean

Statistics

Metric	Count
Definitions `IsAddFreimanHom`, `IsAddFreimanIso`, `IsMulFreimanHom`, `IsMulFreimanIso`	4
Theorems `isAddFreimanIso`, `isAddFreimanHom`, `isAddFreimanIso_Iic`, `isAddFreimanIso_Iio`, `add`, `add_eq_add`, `comp`, `map_sum_eq_map_sum`, `mapsTo`, `mono`, `neg`, `prodMap`, `sub`, `subset`, `subtypeVal`, `superset`, `add_eq_add`, `bijOn`, `comp`, `isAddFreimanHom`, `map_sum_eq_map_sum`, `mono`, `prodMap`, `subset`, `comp`, `div`, `inv`, `map_prod_eq_map_prod`, `mapsTo`, `mono`, `mul`, `mul_eq_mul`, `prodMap`, `subset`, `subtypeVal`, `superset`, `bijOn`, `comp`, `isMulFreimanHom`, `map_prod_eq_map_prod`, `mono`, `mul_eq_mul`, `prodMap`, `subset`, `isMulFreimanHom`, `isMulFreimanIso`, `isAddFreimanHom_const`, `isAddFreimanHom_empty`, `isAddFreimanHom_id`, `isAddFreimanHom_one_iff`, `isAddFreimanHom_two`, `isAddFreimanHom_zero_iff`, `isAddFreimanIso_empty`, `isAddFreimanIso_id`, `isAddFreimanIso_one_iff`, `isAddFreimanIso_two`, `isAddFreimanIso_zero_iff`, `isMulFreimanHom_const`, `isMulFreimanHom_empty`, `isMulFreimanHom_id`, `isMulFreimanHom_one_iff`, `isMulFreimanHom_two`, `isMulFreimanHom_zero_iff`, `isMulFreimanIso_empty`, `isMulFreimanIso_id`, `isMulFreimanIso_one_iff`, `isMulFreimanIso_two`, `isMulFreimanIso_zero_iff`	68
Total	72

AddEquivClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isAddFreimanIso` 📖	mathematical	`Set.BijOn` `DFunLike.coe` `EquivLike.toFunLike`	`IsAddFreimanIso`	—	`map_multiset_sum` `instAddMonoidHomClass` `EquivLike.apply_eq_iff_eq`

AddMonoidHomClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isAddFreimanHom` 📖	mathematical	`Set.MapsTo` `DFunLike.coe`	`IsAddFreimanHom`	—	`map_multiset_sum`

Fin

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isAddFreimanIso_Iic` 📖	mathematical	—	`IsAddFreimanIso` `addCommMonoid` `Nat.instAddCommMonoid` `Set.Iic` `PartialOrder.toPreorder` `instPartialOrder` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `instCommRing` `Nat.instPreorder`	—	`Function.Injective.injOn` `val_injective` `LE.le.trans_lt` `eq_natCast` `RingHom.instRingHomClass` `Nat.cast_multiset_sum` `Multiset.map_map` `Multiset.map_congr` `cast_val_eq_self` `Multiset.map_id'` `LE.le.trans'` `Multiset.card_map` `Multiset.sum_le_card_nsmul` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `CharP.natCast_injOn_Iio` `charP` `AddRightCancelSemigroup.toIsRightCancelAdd`
`isAddFreimanIso_Iio` 📖	mathematical	—	`IsAddFreimanIso` `addCommMonoid` `Nat.instAddCommMonoid` `Set.Iio` `PartialOrder.toPreorder` `instPartialOrder` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `instCommRing` `Nat.instPreorder`	—	`Nat.cast_zero` `IsMin.Iio_eq` `LE.le.trans` `Set.ext` `Nat.cast_add` `Nat.cast_one` `val_cast_of_lt` `isAddFreimanIso_Iic`

IsAddFreimanHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`IsAddFreimanHom`	`Set` `Set.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Pi.instAdd`	—	`Set.MapsTo.add` `mapsTo` `Pi.add_def` `Multiset.sum_map_add` `map_sum_eq_map_sum`
`add_eq_add` 📖	—	`IsAddFreimanHom` `Set` `Set.instMembership` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	—	`Multiset.sum_pair` `map_sum_eq_map_sum` `Multiset.mem_cons` `Multiset.mem_singleton` `Multiset.card_pair`
`comp` 📖	—	`IsAddFreimanHom`	—	—	`Set.MapsTo.comp` `mapsTo` `Multiset.map_map` `map_sum_eq_map_sum` `Multiset.mem_map` `Multiset.card_map`
`map_sum_eq_map_sum` 📖	mathematical	`IsAddFreimanHom` `Set` `Set.instMembership` `Multiset.card` `Multiset.sum`	`Multiset.map`	—	—
`mapsTo` 📖	mathematical	`IsAddFreimanHom`	`Set.MapsTo`	—	—
`mono` 📖	—	`IsAddFreimanHom` `AddCancelCommMonoid.toAddCommMonoid`	—	—	`mapsTo` `Multiset.card_eq_zero` `Multiset.card_pos_iff_exists_mem` `map_sum_eq_map_sum` `Multiset.mem_add` `Multiset.eq_of_mem_replicate` `Multiset.card_add` `Multiset.card_replicate` `Multiset.sum_add` `add_right_cancel` `AddRightCancelSemigroup.toIsRightCancelAdd` `Multiset.map_add`
`neg` 📖	mathematical	`IsAddFreimanHom` `SubtractionCommMonoid.toAddCommMonoid`	`Set` `Set.neg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `Pi.instNeg`	—	`Set.MapsTo.neg` `mapsTo` `Pi.neg_def` `Multiset.sum_map_neg` `map_sum_eq_map_sum`
`prodMap` 📖	mathematical	`IsAddFreimanHom`	`Prod.instAddCommMonoid` `SProd.sprod` `Set` `Set.instSProd`	—	`Set.MapsTo.prodMap` `mapsTo` `Multiset.fst_sum` `Multiset.map_map` `Multiset.map_congr` `Multiset.snd_sum` `map_sum_eq_map_sum` `Multiset.mem_map` `Set.mem_prod` `Multiset.card_map` `forall_swap`
`sub` 📖	mathematical	`IsAddFreimanHom` `SubtractionCommMonoid.toAddCommMonoid`	`Set` `Set.sub` `SubNegMonoid.toSub` `SubtractionMonoid.toSubNegMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `Pi.instSub`	—	`Set.MapsTo.sub` `mapsTo` `Pi.sub_def` `Multiset.sum_map_sub` `map_sum_eq_map_sum`
`subset` 📖	—	`Set` `Set.instHasSubset` `IsAddFreimanHom` `Set.MapsTo`	—	—	`comp` `isAddFreimanHom_id` `map_sum_eq_map_sum`
`subtypeVal` 📖	mathematical	—	`IsAddFreimanHom` `SetLike.instMembership` `AddSubmonoidClass.toAddCommMonoid` `Set.univ`	—	`AddMonoidHomClass.isAddFreimanHom` `AddMonoidHom.instAddMonoidHomClass` `Set.mapsTo_univ`
`superset` 📖	—	`Set` `Set.instHasSubset` `IsAddFreimanHom`	—	—	`comp` `isAddFreimanHom_id`

IsAddFreimanIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_eq_add` 📖	mathematical	`IsAddFreimanIso` `Set` `Set.instMembership`	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`Multiset.sum_pair` `map_sum_eq_map_sum` `Multiset.mem_cons` `Multiset.mem_singleton` `Multiset.card_pair`
`bijOn` 📖	mathematical	`IsAddFreimanIso`	`Set.BijOn`	—	—
`comp` 📖	—	`IsAddFreimanIso`	—	—	`Set.BijOn.comp` `bijOn` `Multiset.map_map` `map_sum_eq_map_sum` `Multiset.mem_map` `Set.BijOn.mapsTo` `Multiset.card_map`
`isAddFreimanHom` 📖	mathematical	`IsAddFreimanIso`	`IsAddFreimanHom`	—	`Set.BijOn.mapsTo` `bijOn` `map_sum_eq_map_sum`
`map_sum_eq_map_sum` 📖	mathematical	`IsAddFreimanIso` `Set` `Set.instMembership` `Multiset.card`	`Multiset.sum` `Multiset.map`	—	—
`mono` 📖	—	`IsAddFreimanIso` `AddCancelCommMonoid.toAddCommMonoid`	—	—	`bijOn` `Multiset.map_congr` `Multiset.card_eq_zero` `Multiset.card_pos_iff_exists_mem` `map_sum_eq_map_sum` `Multiset.mem_add` `Multiset.eq_of_mem_replicate` `Multiset.card_add` `Multiset.card_replicate` `Multiset.map_add` `Multiset.sum_add` `add_right_cancel_iff` `AddRightCancelSemigroup.toIsRightCancelAdd`
`prodMap` 📖	mathematical	`IsAddFreimanIso`	`Prod.instAddCommMonoid` `SProd.sprod` `Set` `Set.instSProd`	—	`Set.BijOn.prodMap` `bijOn` `Multiset.fst_sum` `Multiset.map_map` `Multiset.map_congr` `Multiset.snd_sum` `map_sum_eq_map_sum` `Multiset.mem_map` `Set.mem_prod` `Multiset.card_map` `forall_swap`
`subset` 📖	—	`Set` `Set.instHasSubset` `IsAddFreimanIso` `Set.BijOn`	—	—	`map_sum_eq_map_sum`

IsMulFreimanHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	—	`IsMulFreimanHom`	—	—	`Set.MapsTo.comp` `mapsTo` `Multiset.map_map` `map_prod_eq_map_prod` `Multiset.card_map`
`div` 📖	mathematical	`IsMulFreimanHom` `DivisionCommMonoid.toCommMonoid`	`Set` `Set.div` `DivInvMonoid.toDiv` `DivisionMonoid.toDivInvMonoid` `DivisionCommMonoid.toDivisionMonoid` `Pi.instDiv`	—	`Set.MapsTo.div` `mapsTo` `Pi.div_def` `Multiset.prod_map_div` `map_prod_eq_map_prod`
`inv` 📖	mathematical	`IsMulFreimanHom` `DivisionCommMonoid.toCommMonoid`	`Set` `Set.inv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `Pi.instInv`	—	`Set.MapsTo.inv` `mapsTo` `Pi.inv_def` `Multiset.prod_map_inv` `map_prod_eq_map_prod`
`map_prod_eq_map_prod` 📖	mathematical	`IsMulFreimanHom` `Set` `Set.instMembership` `Multiset.card` `Multiset.prod`	`Multiset.map`	—	—
`mapsTo` 📖	mathematical	`IsMulFreimanHom`	`Set.MapsTo`	—	—
`mono` 📖	—	`IsMulFreimanHom` `CancelCommMonoid.toCommMonoid`	—	—	`mapsTo` `Multiset.card_eq_zero` `map_prod_eq_map_prod` `Multiset.mem_add` `Multiset.eq_of_mem_replicate` `Multiset.card_add` `Multiset.card_replicate` `Multiset.prod_add` `mul_right_cancel` `RightCancelSemigroup.toIsRightCancelMul` `Multiset.map_add`
`mul` 📖	mathematical	`IsMulFreimanHom`	`Set` `Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `Pi.instMul`	—	`Set.MapsTo.mul` `mapsTo` `Pi.mul_def` `Multiset.prod_map_mul` `map_prod_eq_map_prod`
`mul_eq_mul` 📖	—	`IsMulFreimanHom` `Set` `Set.instMembership` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	—	—	`map_prod_eq_map_prod` `Multiset.card_pair`
`prodMap` 📖	mathematical	`IsMulFreimanHom`	`Prod.instCommMonoid` `SProd.sprod` `Set` `Set.instSProd`	—	`Set.MapsTo.prodMap` `mapsTo` `Multiset.fst_prod` `Multiset.map_map` `Multiset.map_congr` `Multiset.snd_prod` `map_prod_eq_map_prod` `Multiset.card_map` `forall_swap`
`subset` 📖	—	`Set` `Set.instHasSubset` `IsMulFreimanHom` `Set.MapsTo`	—	—	`comp` `isMulFreimanHom_id` `map_prod_eq_map_prod`
`subtypeVal` 📖	mathematical	—	`IsMulFreimanHom` `SetLike.instMembership` `SubmonoidClass.toCommMonoid` `Set.univ`	—	`MonoidHomClass.isMulFreimanHom` `MonoidHom.instMonoidHomClass` `Set.mapsTo_univ`
`superset` 📖	—	`Set` `Set.instHasSubset` `IsMulFreimanHom`	—	—	`comp` `isMulFreimanHom_id`

IsMulFreimanIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bijOn` 📖	mathematical	`IsMulFreimanIso`	`Set.BijOn`	—	—
`comp` 📖	—	`IsMulFreimanIso`	—	—	`Set.BijOn.comp` `bijOn` `Multiset.map_map` `map_prod_eq_map_prod` `Set.BijOn.mapsTo` `Multiset.card_map`
`isMulFreimanHom` 📖	mathematical	`IsMulFreimanIso`	`IsMulFreimanHom`	—	`Set.BijOn.mapsTo` `bijOn` `map_prod_eq_map_prod`
`map_prod_eq_map_prod` 📖	mathematical	`IsMulFreimanIso` `Set` `Set.instMembership` `Multiset.card`	`Multiset.prod` `Multiset.map`	—	—
`mono` 📖	—	`IsMulFreimanIso` `CancelCommMonoid.toCommMonoid`	—	—	`bijOn` `Multiset.map_congr` `Multiset.card_eq_zero` `map_prod_eq_map_prod` `Multiset.mem_add` `Multiset.eq_of_mem_replicate` `Multiset.card_add` `Multiset.card_replicate` `Multiset.map_add` `Multiset.prod_add` `RightCancelSemigroup.toIsRightCancelMul`
`mul_eq_mul` 📖	mathematical	`IsMulFreimanIso` `Set` `Set.instMembership`	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	—	`map_prod_eq_map_prod` `Multiset.card_pair`
`prodMap` 📖	mathematical	`IsMulFreimanIso`	`Prod.instCommMonoid` `SProd.sprod` `Set` `Set.instSProd`	—	`Set.BijOn.prodMap` `bijOn` `Multiset.fst_prod` `Multiset.map_map` `Multiset.map_congr` `Multiset.snd_prod` `map_prod_eq_map_prod` `Multiset.card_map` `forall_swap`
`subset` 📖	—	`Set` `Set.instHasSubset` `IsMulFreimanIso` `Set.BijOn`	—	—	`map_prod_eq_map_prod`

MonoidHomClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isMulFreimanHom` 📖	mathematical	`Set.MapsTo` `DFunLike.coe`	`IsMulFreimanHom`	—	`map_multiset_prod`

MulEquivClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isMulFreimanIso` 📖	mathematical	`Set.BijOn` `DFunLike.coe` `EquivLike.toFunLike`	`IsMulFreimanIso`	—	`map_multiset_prod` `instMonoidHomClass` `EquivLike.apply_eq_iff_eq`

(root)

Definitions

Name	Category	Theorems
`IsAddFreimanHom` 📖	CompData	9 math math: `IsAddFreimanHom.subtypeVal`, `isAddFreimanHom_empty`, `isAddFreimanHom_two`, `AddMonoidHomClass.isAddFreimanHom`, `isAddFreimanHom_const`, `IsAddFreimanIso.isAddFreimanHom`, `isAddFreimanHom_id`, `isAddFreimanHom_zero_iff`, `isAddFreimanHom_one_iff`
`IsAddFreimanIso` 📖	CompData	8 math math: `Fin.isAddFreimanIso_Iio`, `isAddFreimanIso_zero_iff`, `isAddFreimanIso_empty`, `Fin.isAddFreimanIso_Iic`, `isAddFreimanIso_one_iff`, `isAddFreimanIso_two`, `isAddFreimanIso_id`, `AddEquivClass.isAddFreimanIso`
`IsMulFreimanHom` 📖	CompData	9 math math: `MonoidHomClass.isMulFreimanHom`, `isMulFreimanHom_one_iff`, `isMulFreimanHom_zero_iff`, `isMulFreimanHom_two`, `IsMulFreimanHom.subtypeVal`, `isMulFreimanHom_empty`, `isMulFreimanHom_id`, `isMulFreimanHom_const`, `IsMulFreimanIso.isMulFreimanHom`
`IsMulFreimanIso` 📖	CompData	6 math math: `isMulFreimanIso_zero_iff`, `MulEquivClass.isMulFreimanIso`, `isMulFreimanIso_one_iff`, `isMulFreimanIso_two`, `isMulFreimanIso_empty`, `isMulFreimanIso_id`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isAddFreimanHom_const` 📖	mathematical	`Set` `Set.instMembership`	`IsAddFreimanHom`	—	`Multiset.map_const'` `Multiset.sum_replicate`
`isAddFreimanHom_empty` 📖	mathematical	—	`IsAddFreimanHom` `Set` `Set.instEmptyCollection`	—	`Set.mapsTo_empty` `Multiset.map_congr` `Multiset.eq_zero_of_forall_notMem` `Set.mem_empty_iff_false` `Multiset.notMem_zero`
`isAddFreimanHom_id` 📖	mathematical	`Set` `Set.instHasSubset`	`IsAddFreimanHom`	—	`Multiset.map_congr` `Multiset.map_id'`
`isAddFreimanHom_one_iff` 📖	mathematical	—	`IsAddFreimanHom` `Set.MapsTo`	—	`IsAddFreimanHom.mapsTo` `Multiset.card_eq_one` `Multiset.map_congr` `Multiset.sum_singleton`
`isAddFreimanHom_two` 📖	mathematical	—	`IsAddFreimanHom` `Set.MapsTo` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`IsAddFreimanHom.mapsTo` `IsAddFreimanHom.add_eq_add` `Multiset.card_eq_two` `Multiset.map_cons` `Multiset.sum_cons` `Multiset.sum_singleton` `Multiset.mem_cons` `Multiset.mem_singleton`
`isAddFreimanHom_zero_iff` 📖	mathematical	—	`IsAddFreimanHom` `Set.MapsTo`	—	`IsAddFreimanHom.mapsTo` `Multiset.card_eq_zero` `Multiset.map_congr`
`isAddFreimanIso_empty` 📖	mathematical	—	`IsAddFreimanIso` `Set` `Set.instEmptyCollection`	—	`Set.bijOn_empty` `Multiset.eq_zero_of_forall_notMem` `Multiset.map_congr`
`isAddFreimanIso_id` 📖	mathematical	—	`IsAddFreimanIso`	—	`Set.bijOn_id` `Multiset.map_congr` `Multiset.map_id'`
`isAddFreimanIso_one_iff` 📖	mathematical	—	`IsAddFreimanIso` `Set.BijOn`	—	`IsAddFreimanIso.bijOn` `Multiset.card_eq_one` `Multiset.sum_singleton` `Multiset.mem_singleton`
`isAddFreimanIso_two` 📖	mathematical	—	`IsAddFreimanIso` `Set.BijOn` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`IsAddFreimanIso.bijOn` `IsAddFreimanIso.add_eq_add` `Multiset.card_eq_two` `Multiset.map_cons` `Multiset.sum_cons` `Multiset.sum_singleton` `Multiset.mem_cons` `Multiset.mem_singleton`
`isAddFreimanIso_zero_iff` 📖	mathematical	—	`IsAddFreimanIso` `Set.BijOn`	—	`IsAddFreimanIso.bijOn` `Multiset.card_eq_zero` `Multiset.map_congr`
`isMulFreimanHom_const` 📖	mathematical	`Set` `Set.instMembership`	`IsMulFreimanHom`	—	`Multiset.map_const'` `Multiset.prod_replicate`
`isMulFreimanHom_empty` 📖	mathematical	—	`IsMulFreimanHom` `Set` `Set.instEmptyCollection`	—	`Set.mapsTo_empty` `Multiset.map_congr` `Multiset.eq_zero_of_forall_notMem`
`isMulFreimanHom_id` 📖	mathematical	`Set` `Set.instHasSubset`	`IsMulFreimanHom`	—	`Multiset.map_congr` `Multiset.map_id'`
`isMulFreimanHom_one_iff` 📖	mathematical	—	`IsMulFreimanHom` `Set.MapsTo`	—	`IsMulFreimanHom.mapsTo` `Multiset.map_congr` `Multiset.prod_singleton`
`isMulFreimanHom_two` 📖	mathematical	—	`IsMulFreimanHom` `Set.MapsTo` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	—	`IsMulFreimanHom.mapsTo` `IsMulFreimanHom.mul_eq_mul` `Multiset.map_cons` `Multiset.prod_cons` `Multiset.prod_singleton`
`isMulFreimanHom_zero_iff` 📖	mathematical	—	`IsMulFreimanHom` `Set.MapsTo`	—	`IsMulFreimanHom.mapsTo` `Multiset.map_congr`
`isMulFreimanIso_empty` 📖	mathematical	—	`IsMulFreimanIso` `Set` `Set.instEmptyCollection`	—	`Set.bijOn_empty` `Multiset.eq_zero_of_forall_notMem` `Multiset.map_congr`
`isMulFreimanIso_id` 📖	mathematical	—	`IsMulFreimanIso`	—	`Set.bijOn_id` `Multiset.map_congr` `Multiset.map_id'`
`isMulFreimanIso_one_iff` 📖	mathematical	—	`IsMulFreimanIso` `Set.BijOn`	—	`IsMulFreimanIso.bijOn` `Multiset.prod_singleton`
`isMulFreimanIso_two` 📖	mathematical	—	`IsMulFreimanIso` `Set.BijOn` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	—	`IsMulFreimanIso.bijOn` `IsMulFreimanIso.mul_eq_mul` `Multiset.map_cons` `Multiset.prod_cons` `Multiset.prod_singleton`
`isMulFreimanIso_zero_iff` 📖	mathematical	—	`IsMulFreimanIso` `Set.BijOn`	—	`IsMulFreimanIso.bijOn` `Multiset.map_congr`

---

← Back to Index