Lean4
/-- Turn a homomorphism between unit groups into a `MulChar`. -/
noncomputable def ofUnitHom (f : Rˣ →* R'ˣ) : MulChar R R'
where
toFun := by classical exact fun x => if hx : IsUnit x then f hx.unit else 0
map_one' := by
have h1 : (isUnit_one.unit : Rˣ) = 1 := Units.ext rfl
simp only [h1, dif_pos, Units.val_eq_one, map_one, isUnit_one]
map_mul' := by
classical
intro x y
by_cases hx : IsUnit x
· simp only [hx, IsUnit.mul_iff, true_and, dif_pos]
by_cases hy : IsUnit y
· simp only [hy, dif_pos]
have hm : (hx.mul hy).unit = hx.unit * hy.unit := Units.ext rfl
rw [hm, map_mul]
norm_cast
· simp only [hy, not_false_iff, dif_neg, mul_zero]
· simp only [hx, IsUnit.mul_iff, false_and, not_false_iff, dif_neg, zero_mul]
map_nonunit' := by
intro a ha
simp only [ha, not_false_iff, dif_neg]
