English
If m ≤ n and IsMulFreimanIso n A B f holds, then IsMulFreimanIso m A B f also holds.
Русский
Если m ≤ n и IsMulFreimanIso n A B f выполняется, то и IsMulFreimanIso m A B f выполняется.
LaTeX
$$$m \\le n \\Rightarrow IsMulFreimanIso n A B f \\Rightarrow IsMulFreimanIso m A B f$$$
Lean4
@[to_additive]
theorem mono {hmn : m ≤ n} (hf : IsMulFreimanIso n A B f) : IsMulFreimanIso m A B f
where
bijOn := hf.bijOn
map_prod_eq_map_prod s t hsA htA hs
ht := by
obtain rfl | hm := m.eq_zero_or_pos
· rw [card_eq_zero] at hs ht
simp [hs, ht]
simp only [← hs, card_pos_iff_exists_mem] at hm
obtain ⟨a, ha⟩ := hm
suffices
((s + replicate (n - m) a).map f).prod = ((t + replicate (n - m) a).map f).prod ↔
(s + replicate (n - m) a).prod = (t + replicate (n - m) a).prod
by simpa only [Multiset.map_add, prod_add, mul_right_cancel_iff] using this
replace ha := hsA ha
refine hf.map_prod_eq_map_prod (fun a ha ↦ ?_) (fun a ha ↦ ?_) ?_ ?_
· rw [Multiset.mem_add] at ha
obtain ha | ha := ha
· exact hsA ha
· rwa [eq_of_mem_replicate ha]
· rw [Multiset.mem_add] at ha
obtain ha | ha := ha
· exact htA ha
· rwa [eq_of_mem_replicate ha]
· rw [card_add, card_replicate, hs, Nat.add_sub_cancel' hmn]
· rw [card_add, card_replicate, ht, Nat.add_sub_cancel' hmn]
