Theorems · Inductive type · group theory

AddConstMap

(G : Type u_1) → (H : Type u_2) → [Add G] → [Add H] → G → H → Type (max u_1 u_2)

A bundled map f : G → H such that f (x + a) = f x + b for all x, denoted as f : G →+c[a, b] H. One can think about f as a lift to G of a map between two AddCircles.

Defined in

Mathlib.Algebra.AddConstMap.Basic

Cited by

32 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

AddAdd