Theorems · Theorem · real analysis

MonoidWithZeroHom.mk.congr_simp

∀ {α : Type u_7} {β : Type u_8} [inst : MulZeroOneClass α] [inst_1 : MulZeroOneClass β]
  (toZeroHom toZeroHom_1 : ZeroHom α β) (e_toZeroHom : toZeroHom = toZeroHom_1) (map_one' : toZeroHom.toFun 1 = 1)
  (map_mul' : ∀ (x y : α), toZeroHom.toFun (x * y) = toZeroHom.toFun x * toZeroHom.toFun y),
  { toZeroHom := toZeroHom, map_one' := map_one', map_mul' := map_mul' } =
    { toZeroHom := toZeroHom_1, map_one' := ⋯, map_mul' := ⋯ }

Defined in

Mathlib.Analysis.Real.Sqrt

Cited by

8 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms

Assumes

MulZeroOneClassMulZeroOneClass